From: Enrico Tassi Date: Mon, 26 May 2008 09:46:16 +0000 (+0000) Subject: auto syntax updated X-Git-Tag: make_still_working~5132 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f569c2d610c176b1d85de41968c2f3fbe2aef4e2;p=helm.git auto syntax updated --- diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index 764723261..812c8ed97 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -184,7 +184,8 @@ Synopsis: - auto &autoparams; + auto &autoparams;. + autobatch &autoparams; @@ -195,7 +196,8 @@ controlled by the optional params. Moreover, only lemmas whose type signature is a subset of the signature of the current sequent are considered. The signature of - a sequent is ...&TODO; + a sequent is essentially the set of constats appearing in it. + diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 15793c63a..592e583e4 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -737,9 +737,8 @@ ::= [&simpleautoparam;]… [by - &term; [&term;]…] + &term;, [&term;]…] - &TODO; @@ -752,19 +751,34 @@ &simpleautoparam; ::= depth=&nat; - &TODO; + Give a bound to the depth of the search tree | width=&nat; - &TODO; + The maximal width of the search tree | - &TODO; - &TODO; + library + Search everywhere (not only in included files) + + + + | + type + Try to close also goals of sort Type, otherwise only goals + living in sort Prop are attacked. + + + + + | + paramodulation + Try to close the goal performing unit-equality paramodulation + diff --git a/helm/software/matita/help/C/tactics_quickref.xml b/helm/software/matita/help/C/tactics_quickref.xml index 331d58dc2..a7c1ae3bd 100644 --- a/helm/software/matita/help/C/tactics_quickref.xml +++ b/helm/software/matita/help/C/tactics_quickref.xml @@ -29,7 +29,7 @@ | - auto auto_params + auto auto_params. autobatch auto_params