- init_cache_and_tables rewritten using the automation_cache

[helm.git] / helm / software / matita / library / demo / propositional_sequent_calculus.ma

diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
index 6e389c2fa1ac8227d1c17730715f7fe5af0b709f..5e337d1b801370f83f2af25ad699f7db3a2eddda 100644 (file)
--- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma
+++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
@@ -242,11 +242,13 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F).
     lapply (H4 i); clear H4;
     rewrite > symm_orb in ⊢ (? ? (? ? %) ?);
     rewrite > distributive_orb_andb;
+    STOP
     autobatch paramodulation
   | simplify in H2 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
-    autobatch
+    pump 98.
+    autobatch.
   | simplify in H2 H4 ⊢ %;
     intros;
     lapply (H2 i); clear H2;