X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=01d9ea63e32cb82e1cd27895f849e9cc08a0b21c;hb=aaefdd61e5a4bf25645812676c977a5a863daa33;hp=fb695879f35cb92c8748f9b937647b8ce0b5fbd6;hpb=ebd137ecfde1fe0b10e32a939d2abd65d482a4c1;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index fb695879f..01d9ea63e 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 &term;
+ absurd &sterm;
absurd
absurd P
@@ -33,7 +33,7 @@
- apply &term;
+ 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 &term;
+ 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 &term; [as &id;]
+ cut &sterm; [as &id;]
cut
cut P as H
@@ -312,7 +312,7 @@
- decompose &id; [&id;]⦠[<intros_spec>]
+ decompose &id; [&id;]⦠[<intros_spec>]
decompose
decompose ???
@@ -339,7 +339,7 @@
- discriminate &term;
+ discriminate &sterm;
discriminate
discriminate p
@@ -368,7 +368,7 @@ its constructor takes no arguments.
- elim &term; [using &term;] [<intros_spec>]
+ elim &sterm; [using &sterm;] [<intros_spec>]
elim
elim t using th hyps
@@ -405,7 +405,7 @@ its constructor takes no arguments.
- elimType &term; [using &term;] [<intros_spec>]
+ elimType &sterm; [using &sterm;] [<intros_spec>]
elimType
elimType T using th hyps
@@ -432,7 +432,7 @@ its constructor takes no arguments.
- exact &term;
+ exact &sterm;
exact
exact p
@@ -460,7 +460,7 @@ its constructor takes no arguments.
- exists
+ exists
exists
exists
@@ -491,8 +491,8 @@ its constructor takes no arguments.
- fail
- failt
+ fail
+ fail
fail
@@ -518,7 +518,7 @@ its constructor takes no arguments.
- fold <reduction_kind> &term; <pattern>
+ fold <reduction_kind> &sterm; <pattern>
fold
fold red t patt
@@ -550,7 +550,7 @@ its constructor takes no arguments.
- fourier
+ fourier
fourier
fourier
@@ -580,7 +580,7 @@ its constructor takes no arguments.
- fwd &id; [<ident list>]
+ fwd &id; [<ident list>]
fwd
fwd ...TODO
@@ -607,7 +607,7 @@ its constructor takes no arguments.
- generalize <pattern> [as &id;]
+ generalize <pattern> [as &id;]
generalize
generalize patt as H
@@ -643,7 +643,7 @@ its constructor takes no arguments.
- id
+ id
id
id
@@ -670,8 +670,8 @@ its constructor takes no arguments.
- injection &term;
- injection
+ injection &sterm;
+ injection
injection p
@@ -701,7 +701,7 @@ its constructor takes no arguments.
- intro [&id;]
+ intro [&id;]
intro
intro H
@@ -734,7 +734,7 @@ its constructor takes no arguments.
- intros <intros_spec>
+ intros <intros_spec>
intros
intros hyps
@@ -771,7 +771,7 @@ its constructor takes no arguments.
- inversion &term;
+ inversion &sterm;
inversion
inversion t
@@ -806,7 +806,7 @@ its constructor takes no arguments.
- lapply [depth=&nat;] &term; [to <term list>] [using &id;]
+ lapply [depth=&nat;] &sterm; [to <term list>] [using &id;]
lapply
lapply ???
@@ -833,7 +833,7 @@ its constructor takes no arguments.
- left
+ left
left
left
@@ -864,7 +864,7 @@ its constructor takes no arguments.
- letin &id; â &term;
+ letin &id; â &sterm;
letin
letin x â t
@@ -892,7 +892,7 @@ its constructor takes no arguments.
- normalize <pattern>
+ normalize <pattern>
normalize
normalize patt
@@ -920,7 +920,7 @@ its constructor takes no arguments.
- paramodulation <pattern>
+ paramodulation <pattern>
paramodulation
paramodulation patt
@@ -947,7 +947,7 @@ its constructor takes no arguments.
- reduce <pattern>
+ reduce <pattern>
reduce
reduce patt
@@ -975,7 +975,7 @@ its constructor takes no arguments.
- reflexivity
+ reflexivity
reflexivity
reflexivity
@@ -1004,7 +1004,7 @@ its constructor takes no arguments.
- replace <pattern> with &term;
+ replace <pattern> with &sterm;
change
change patt with t
@@ -1036,7 +1036,7 @@ its constructor takes no arguments.
- rewrite [<|>] &term; <pattern>
+ rewrite [<|>] &sterm; <pattern>
rewrite
rewrite dir p patt
@@ -1071,7 +1071,7 @@ its constructor takes no arguments.
- right
+ right
right
right
@@ -1102,7 +1102,7 @@ its constructor takes no arguments.
- ring
+ ring
ring
ring
@@ -1133,7 +1133,7 @@ its constructor takes no arguments.
- simplify <pattern>
+ simplify <pattern>
simplify
simplify patt
@@ -1161,7 +1161,7 @@ its constructor takes no arguments.
- split
+ split
split
split
@@ -1192,7 +1192,7 @@ its constructor takes no arguments.
- symmetry
+ symmetry
symmetry
The tactic symmetry
symmetry
@@ -1221,7 +1221,7 @@ its constructor takes no arguments.
- transitivity &term;
+ transitivity &sterm;
transitivity
transitivity t
@@ -1250,7 +1250,7 @@ the current sequent to prove.
- unfold [&term;] <pattern>
+ unfold [&sterm;] <pattern>
unfold
unfold t patt
@@ -1282,7 +1282,7 @@ the current sequent to prove.
- whd <pattern>
+ whd <pattern>
whd
whd patt