X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_tactics.xml;h=e9f1567239ef53add4626f8705f6f3d37391d415;hb=f90f8c9a11c19b882a8fbe4aea6bf46f7751c2f1;hp=bc5095fae94061d264bf51662680b1da622db51f;hpb=a094832a413d3d11cd4031b01a5119452384a7ac;p=helm.git
diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index bc5095fae..e9f156723 100644
--- a/matita/help/C/sec_tactics.xml
+++ b/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.
@@ -1197,39 +1232,6 @@ its constructor takes no arguments.
-
- paramodulation
- paramodulation
- paramodulation patt
-
-
-
- Synopsis:
-
- paramodulation &pattern;
-
-
-
- Pre-conditions:
-
- TODO.
-
-
-
- Action:
-
- TODO.
-
-
-
- New sequents to prove:
-
- TODO.
-
-
-
-
-
reduce
reduce