From: Claudio Sacerdoti Coen Date: Fri, 18 Nov 2011 15:17:05 +0000 (+0000) Subject: Auto parameters documented for 0.99.1. X-Git-Tag: make_still_working~2087 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68aad189a157255485177a8a632d44ac3ad73a09;p=helm.git Auto parameters documented for 0.99.1. --- diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml index 8e680bb7c..9a968e5c9 100644 --- a/matita/matita/help/C/sec_terms.xml +++ b/matita/matita/help/C/sec_terms.xml @@ -752,9 +752,20 @@ &autoparams; ::= - [&simpleautoparam;]… + [&nat;] [&simpleautoparam;]… [by - &term; [,&term;]…] + [&sterm;… | _]] + + The natural number, which defaults to 1, gives a bound to + the depth of the search tree. The terms listed is the only + knowledge base used by automation together with all indexed factual + and equational theorems in the included library. If the list of terms + is empty, only equational theorems and facts in the library are + used. If the list is omitted, it defaults to all indexed theorems + in the library. Finally, if the list is _, + the automation command becomes a macro that is expanded in a new + automation command where _ is replaced with the + list of theorems required to prove the sequent. @@ -767,47 +778,35 @@ &simpleautoparam; ::= - depth=&nat; - Give a bound to the depth of the search tree - - - - | width=&nat; The maximal width of the search tree | - library - Search everywhere (not only in included files) + size=&nat; + The maximal number of nodes in the proof | - type - Try to close also goals of sort Type, otherwise only goals - living in sort Prop are attacked. + demod + Simplifies the current sequent using the current set of + equations known to automation | - paramodulation + paramod Try to close the goal performing unit-equality paramodulation | - size=&nat; - The maximal number of nodes in the proof - - - - | - timeout=&nat; - Timeout in seconds + fast_paramod + A bounded version of paramod that is granted to terminate quickly