From: Ferruccio Guidi Date: Thu, 7 May 2009 14:30:26 +0000 (+0000) Subject: documentation for the inline command X-Git-Tag: make_still_working~4013 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8caf14a7b9765bea19cf4249530a537fe6fe8d6e;p=helm.git documentation for the inline command --- diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index f66e64093..aa45a806a 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -55,6 +55,8 @@ auto_params"> justification"> simple_auto_param"> + inline_params"> + inline_param"> interpretation_argument"> interpretation_rhs"> csymbol"> diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml index 19685bf90..7e22f3304 100644 --- a/helm/software/matita/help/C/sec_commands.xml +++ b/helm/software/matita/help/C/sec_commands.xml @@ -379,7 +379,7 @@ qed - + qed @@ -401,5 +401,188 @@ - + + + inline + inline "s" params + + + + Synopsis: + + + inline &qstring; &inlineparams; + + + + + Action: + + Inlines a representation of the item s, +which can be the URI of a HELM object. If an entire HELM directory (i.e. a base +URI) or the path of a *.ma source file is provided, all the contained objects +are represented in a row. +If the inlined object has a proof, this proof is represented in several ways +depending on the provided parameters. + + + + + + + inline-params + + inline-params + + + + &inlineparams; + ::= + [&inlineparam; [&inlineparam;] … ] + + + +
+ + inline-param + + + + + &inlineparam; + ::= + axiom + Try to give an axiom flavour + (bodies are omitted even if present) + + + + + + | + definition + Try give a definition flavour + + + + + + | + theorem + Try give a theorem flavour + + + + + + | + lemma + Try give a lemma flavour + + + + + + | + remark + Try give a remark flavour + + + + + | + fact + Try give a fact flavour + + + + + + | + variant + Try give a variant flavour + (implies plain) + + + + + + | + declarative + Represent proofs using + declarative tactics + (this is the dafault and can be omitted) + + + + + + | + procedural + Represent proofs using + procedural tactics + + + + + + | + plain + Represent proofs using plain + proof terms + + + + + + | + nodefaults + + Do not use the tactics depending on the + default command + (rewrite + in the procedural mode) + + + + + + | + level=&nat; + + Set the level of the procedural proof representation + (the default is the highest level) + + + Tactics used at level 1: + exact + + + Additional tactics used at level 2: + letin, + cut, + change, + intros, + apply, + elim, + cases, + rewrite + + + + + + + + | + depth=&nat; + &TODO; + + + + +
+
+
+ diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 2a42fc88d..a1353b2f0 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -140,7 +140,7 @@ --> - +
Terms