Update Arithmetization (Foundation) (#11)

SnO2WMaN · web-flow · commit 57edda8d1a2f · 2024-11-28T21:51:57.000+09:00
diff --git a/Incompleteness.lean b/Incompleteness.lean
@@ -7,4 +7,4 @@ import Incompleteness.Arith.Second
 import Incompleteness.Arith.DC
 import Incompleteness.DC.Basic
 
-import Incompleteness.ProvabilityLogic.ProvabilityLogic
+import Incompleteness.ProvabilityLogic.Basic
diff --git a/Incompleteness/ProvabilityLogic/Basic.lean b/Incompleteness/ProvabilityLogic/Basic.lean
@@ -1,6 +1,6 @@
 import Incompleteness.Arith.DC
 import Incompleteness.DC.Basic
-import Foundation.Modal.Hilbert
+import Foundation.Modal.Hilbert.Systems
 
 namespace LO
 
diff --git a/Incompleteness/ProvabilityLogic/ProvabilityLogic.lean b/Incompleteness/ProvabilityLogic/ProvabilityLogic.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "FormalizedFormalLogic",
-   "rev": "810258379c6c3a47e967817ded9098da662431e7",
+   "rev": "a1bfd1fa480026f05e476050030c0b2d17983bb0",
    "name": "foundation",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "FormalizedFormalLogic",
-   "rev": "de211f4878773176beef6f244a6585c9a43c5982",
+   "rev": "fe2c1952fc091a965b64e2aa5dbcc4581e7497a6",
    "name": "arithmetization",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
