fixed last file restricting auto tables

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 0e43948238dce3d7a7f52335c65c28c2fe1d22c8..1b172786a7a44a071f28079c8dbdf409a8c996ec 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -388,6 +388,8 @@ let init_cache_and_tables
              (List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv))
         automation_cache.AutomationCache.tables ct
     in
+(*     AutomationCache.pp_cache { automation_cache with AutomationCache.tables =
+        *     tables }; *)
     automation_cache.AutomationCache.univ, tables, cache
   else
     let metasenv, t_ty, s_t_ty, _ = 

diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
index 5e337d1b801370f83f2af25ad699f7db3a2eddda..63d64bebc48d1cd7575e499e5cc15430707fb0c0 100644 (file)
--- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma
+++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
@@ -181,6 +181,8 @@ axiom symm_andb: symmetric ? andb.
 axiom associative_andb: associative ? andb.
 axiom distributive_andb_orb: distributive ? andb orb.
 
+lemma andb_true: ∀x.(true ∧ x) = x. intro; reflexivity. qed. 
+
 lemma and_of_list_permut:
  ∀i,f,l1,l2. eval i (and_of_list (l1 @ (f::l2))) = eval i (and_of_list (f :: l1 @ l2)).
  intros;
@@ -242,13 +244,11 @@ 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
+    autobatch paramodulation by distributive_orb_andb,symm_orb,symm_orb, Hletin, Hletin1,andb_true.
   | simplify in H2 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
-    pump 98.
-    autobatch.
+    autobatch paramodulation by andb_assoc, Hletin. 
   | simplify in H2 H4 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
@@ -258,11 +258,11 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F).
     rewrite > demorgan2;
     rewrite > symm_orb;
     rewrite > distributive_orb_andb;
-    autobatch paramodulation
+    autobatch paramodulation by symm_andb,symm_orb,andb_true,Hletin,Hletin1.
   | simplify in H2 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
-    autobatch
+    autobatch paramodulation;
   | simplify in H2 ⊢ %;
     intros;
     lapply (H2 i); clear H2;