From 6d7709145b99cf829ed4084af5b41b82b27dc4b6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 5 Nov 2008 07:37:22 +0000 Subject: [PATCH] fixed script to use auto depth=4 --- .../matita/library/demo/propositional_sequent_calculus.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma index 36bb7e863..6e389c2fa 100644 --- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma +++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma @@ -508,7 +508,7 @@ lemma look_for_axiom: simplify; apply (ex_intro ? ? a3); apply (ex_intro ? ? a4); - autobatch + autobatch depth=4 | right; intro; apply (bool_elim ? (same_atom a (FAtom n1))); -- 2.39.2