Bml: compile it all (but still with sorries - is that a word?)

m4lvin · Oct 30, 2023 · ccd6afc · ccd6afc
1 parent 1a173d6
commit ccd6afc
Show file tree

Hide file tree

Showing 3 changed files with 94 additions and 94 deletions.
diff --git a/Bml.lean b/Bml.lean
@@ -10,5 +10,5 @@ import «Bml».Vocabulary
 import «Bml».Soundness
 import «Bml».Tableauexamples
 import «Bml».Completeness
--- TODO import «Bml».Partitions
--- TODO import «Bml».Interpolation
+import «Bml».Partitions
+import «Bml».Interpolation
diff --git a/Bml/Interpolation.lean b/Bml/Interpolation.lean
@@ -33,4 +33,4 @@ theorem interpolation {ϕ ψ} : Tautology (ϕ↣ψ) → ∃ θ, Interpolant ϕ
   · rw [tautImp_iff_comboNotUnsat]; tauto
   constructor
   · rw [tautImp_iff_comboNotUnsat]; simp at *; tauto
-  · cases pI_prop; unfold voc vocabOfSetFormula at *; simp at *; tauto
+  · cases pI_prop; simp at *; tauto