From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 5 Nov 2008 07:37:22 +0000 (+0000)
Subject: fixed script to use auto depth=4
X-Git-Tag: make_still_working~4600
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d7709145b99cf829ed4084af5b41b82b27dc4b6;p=helm.git

fixed script to use auto depth=4
---

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)));