X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=56037dde56bf7d59f20b4efc6d6b1f848a2b643a;hb=e43d7e9c2acfa6d1c74838ba15589833cfc275fc;hp=bc5095fae94061d264bf51662680b1da622db51f;hpb=a713b1508a5eaa20d1a2051366e3ec6057b7693b;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index bc5095fae..56037dde5 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -163,27 +163,40 @@
clear
clear
- clear H
+
+ clear H1 ... Hm
+
Synopsis:
- clear &id;
+
+ clear
+ &id; [&id;â¦]
+
Pre-conditions:
- H must be an hypothesis of the
- current sequent to prove.
+
+
+ H1 ... Hm
+ must be hypotheses of the
+ current sequent to prove.
+
Action:
- It hides the hypothesis H from the
- current sequent.
+
+ It hides the hypotheses
+
+ H1 ... Hm
+ from the current sequent.
+
@@ -382,7 +395,8 @@
decompose
decompose
- decompose (T1 ... Tn) H hips
+ decompose (T1 ... Tn)
+ H as H1 ... Hm
@@ -391,8 +405,11 @@
decompose
- [([&id;]â¦)]
- &id; &intros-spec;
+ [(
+ &id;â¦
+ )]
+ [&id;]
+ [as &id;â¦]
@@ -412,9 +429,13 @@
Action:
- Runs elim H hyps, clears H and tries to run
- itself recursively on each new identifier introduced by
- elim in the opened sequents.
+ Runs
+ elim H H1 ... Hm
+ , clears H and tries to run itself
+ recursively on each new identifier introduced by
+ elim in the opened sequents.
+ If H is not provided tries this operation on
+ each premise in the current context.
@@ -429,16 +450,16 @@
-
- demodulation
- demodulation
- demodulation patt
+
+ demodulate
+ demodulate
+ demodulate
Synopsis:
- demodulation &pattern;
+ demodulate
@@ -1040,7 +1061,7 @@ its constructor takes no arguments.
lapply
lapply
- lapply depth=d t
+ lapply linear depth=d t
to t1, ..., tn as H
@@ -1048,7 +1069,17 @@ its constructor takes no arguments.
Synopsis:
- lapply [depth=&nat;] &sterm; [to &sterm; [&sterm;]â¦] [as &id;]
+
+ lapply
+ [linear]
+ [depth=&nat;]
+ &sterm;
+ [to
+ &sterm;
+ [,&sterm;â¦]
+ ]
+ [as &id;]
+
@@ -1065,12 +1096,12 @@ its constructor takes no arguments.
Action:
- It invokes letin H â (t ? ... ?)
+ Invokes letin H â (t ? ... ?)
with enough ?'s to reach the
d-th independent premise of
t
(d is maximum if unspecified).
- Then it istantiates (by apply) with
+ Then istantiates (by apply) with
t1, ..., tn
the ?'s corresponding to the first
n independent premises of
@@ -1078,6 +1109,10 @@ its constructor takes no arguments.
Usually the other ?'s preceding the
n-th independent premise of
t are istantiated as a consequence.
+ If the linear flag is specified and if
+ t, t1, ..., tn
+ are (applications of) premises in the current context, they are
+ cleared.