From bdbe077ddb0b377823b6806adc8bece82130c992 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 21 Apr 2009 13:03:55 +0000 Subject: [PATCH] fixed last file restricting auto tables --- helm/software/components/tactics/auto.ml | 2 ++ .../library/demo/propositional_sequent_calculus.ma | 12 ++++++------ 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 0e4394823..1b172786a 100644 --- 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 5e337d1b8..63d64bebc 100644 --- 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; -- 2.39.2