X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=fc3681074429c8f29b7d90b975937df1628332ec;hb=cce6f6dc86e2891f87b2023f35ccc5d73a10a5dd;hp=96e56494ce22d0db5de5a0571d0a2218a1795af8;hpb=b4fb4fa6c17945b70d821e2b31e6aca727bcf9d5;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 96e56494c..fc3681074 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -4,7 +4,7 @@
Tactics
- absurd &sterm;
+ absurd &sterm;
absurd
absurd P
@@ -33,7 +33,7 @@
- apply &sterm;
+ apply &sterm;
apply
apply t
@@ -68,7 +68,7 @@
- assumption
+ assumption
assumption
assumption
@@ -96,7 +96,7 @@
- auto [depth=&nat;] [width=&nat;] [paramodulation] [full]
+ auto [depth=&nat;] [width=&nat;] [paramodulation] [full]
auto
auto depth=d width=w paramodulation full
@@ -130,7 +130,7 @@
- clear &id;
+ clear &id;
clear
clear H
@@ -159,7 +159,7 @@
- clearbody &id;
+ clearbody &id;
clearbody
clearbody H
@@ -188,7 +188,7 @@
- change <pattern> with &sterm;
+ change &pattern; with &sterm;
change
change patt with t
@@ -220,7 +220,7 @@
- constructor &nat;
+ constructor &nat;
constructor
constructor n
@@ -252,7 +252,7 @@
- contradiction
+ contradiction
contradiction
contradiction
@@ -281,7 +281,7 @@
- cut &sterm; [as &id;]
+ cut &sterm; [as &id;]
cut
cut P as H
@@ -312,34 +312,75 @@
- decompose &id; [&id;]⦠[<intros_spec>]
+ decompose &id; [&id;]⦠&intros-spec;
decompose
- decompose ???
+
+ decompose (T1 ... Tn) H hips
+
Pre-conditions:
- TODO.
+
+ H must inhabit one inductive type among
+
+ T1 ... Tn
+
+ and the types of a predefined list.
+
Action:
- TODO.
+
+ Runs elim H hyps, clears H and tries to run
+ itself recursively on each new identifier introduced by
+ elim in the opened sequents.
+
New sequents to prove:
- TODO.
+
+ The ones generated by all the elim tactics run.
+
+
+
+
+
+
+
+ demodulation &pattern;
+ demodulation
+ demodulation patt
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ &TODO;
+
+
+
+ New sequents to prove:
+
+ None.
- discriminate &sterm;
+ discriminate &sterm;
discriminate
discriminate p
@@ -368,7 +409,7 @@ its constructor takes no arguments.
- elim &sterm; [using &sterm;] [<intros_spec>]
+ elim &sterm; [using &sterm;] &intros-spec;
elim
elim t using th hyps
@@ -405,7 +446,7 @@ its constructor takes no arguments.
- elimType &sterm; [using &sterm;] [<intros_spec>]
+ elimType &sterm; [using &sterm;] &intros-spec;
elimType
elimType T using th hyps
@@ -432,7 +473,7 @@ its constructor takes no arguments.
- exact &sterm;
+ exact &sterm;
exact
exact p
@@ -460,7 +501,7 @@ its constructor takes no arguments.
- exists
+ exists
exists
exists
@@ -491,8 +532,8 @@ its constructor takes no arguments.
- fail
- failt
+ fail
+ fail
fail
@@ -518,7 +559,7 @@ its constructor takes no arguments.
- fold <reduction_kind> &sterm; <pattern>
+ fold &reduction-kind; &sterm; &pattern;
fold
fold red t patt
@@ -550,7 +591,7 @@ its constructor takes no arguments.
- fourier
+ fourier
fourier
fourier
@@ -580,7 +621,7 @@ its constructor takes no arguments.
- fwd &id; [<ident list>]
+ fwd &id; [([&id;]â¦)]
fwd
fwd ...TODO
@@ -607,7 +648,7 @@ its constructor takes no arguments.
- generalize <pattern> [as &id;]
+ generalize &pattern; [as &id;]
generalize
generalize patt as H
@@ -643,7 +684,7 @@ its constructor takes no arguments.
- id
+ id
id
id
@@ -670,8 +711,8 @@ its constructor takes no arguments.
- injection &sterm;
- injection
+ injection &sterm;
+ injection
injection p
@@ -701,7 +742,7 @@ its constructor takes no arguments.
- intro [&id;]
+ intro [&id;]
intro
intro H
@@ -734,7 +775,7 @@ its constructor takes no arguments.
- intros <intros_spec>
+ intros &intros-spec;
intros
intros hyps
@@ -771,7 +812,7 @@ its constructor takes no arguments.
- inversion &sterm;
+ inversion &sterm;
inversion
inversion t
@@ -806,9 +847,12 @@ its constructor takes no arguments.
- lapply [depth=&nat;] &sterm; [to <term list>] [using &id;]
+ lapply [depth=&nat;] &sterm; [to &sterm; [&sterm;]â¦] [using &id;]
lapply
- lapply ???
+
+ lapply depth=d t
+ to t1, ..., tn using H
+
@@ -833,7 +877,7 @@ its constructor takes no arguments.
- left
+ left
left
left
@@ -864,7 +908,7 @@ its constructor takes no arguments.
- letin &id; â &sterm;
+ letin &id; â &sterm;
letin
letin x â t
@@ -892,7 +936,7 @@ its constructor takes no arguments.
- normalize <pattern>
+ normalize &pattern;
normalize
normalize patt
@@ -920,7 +964,7 @@ its constructor takes no arguments.
- paramodulation <pattern>
+ paramodulation &pattern;
paramodulation
paramodulation patt
@@ -947,7 +991,7 @@ its constructor takes no arguments.
- reduce <pattern>
+ reduce &pattern;
reduce
reduce patt
@@ -975,7 +1019,7 @@ its constructor takes no arguments.
- reflexivity
+ reflexivity
reflexivity
reflexivity
@@ -1004,7 +1048,7 @@ its constructor takes no arguments.
- replace <pattern> with &sterm;
+ replace &pattern; with &sterm;
change
change patt with t
@@ -1036,7 +1080,7 @@ its constructor takes no arguments.
- rewrite [<|>] &sterm; <pattern>
+ rewrite [<|>] &sterm; &pattern;
rewrite
rewrite dir p patt
@@ -1071,7 +1115,7 @@ its constructor takes no arguments.
- right
+ right
right
right
@@ -1102,7 +1146,7 @@ its constructor takes no arguments.
- ring
+ ring
ring
ring
@@ -1133,7 +1177,7 @@ its constructor takes no arguments.
- simplify <pattern>
+ simplify &pattern;
simplify
simplify patt
@@ -1161,7 +1205,7 @@ its constructor takes no arguments.
- split
+ split
split
split
@@ -1192,7 +1236,7 @@ its constructor takes no arguments.
- symmetry
+ symmetry
symmetry
The tactic symmetry
symmetry
@@ -1221,7 +1265,7 @@ its constructor takes no arguments.
- transitivity &sterm;
+ transitivity &sterm;
transitivity
transitivity t
@@ -1250,7 +1294,7 @@ the current sequent to prove.
- unfold [&sterm;] <pattern>
+ unfold [&sterm;] &pattern;
unfold
unfold t patt
@@ -1282,7 +1326,7 @@ the current sequent to prove.
- whd <pattern>
+ whd &pattern;
whd
whd patt