X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=03842a70904647081e5335656fc3b39534c5316f;hb=543cce4ec3113fc54c6b276713e10fce74cb5f20;hp=9ba73d991ad40a52f37a406a797906a330c0c858;hpb=dd91d9b3909b0f6bfd4c1de701620f46976e61bd;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 9ba73d991..03842a709 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -1,19 +1,19 @@
-
+
Tactics
-
+
absurd <term>
absurd P
-
+
+
Pre-conditions:
P must have type Prop.
-
Action:
@@ -29,9 +29,9 @@
-
-
-
+
+
+
apply <term>
apply t
@@ -64,10 +64,10 @@
-
-
+
+
assumption
- assumption
+ assumption
@@ -91,8 +91,8 @@
-
-
+
+
auto [depth=<int>] [width=<int>] [paramodulation] [full]
auto depth=d width=w paramodulation full
@@ -124,8 +124,8 @@
-
-
+
+
clear <id>
clear H
@@ -152,8 +152,8 @@
-
-
+
+
clearbody <id>
clearbody H
@@ -180,8 +180,8 @@
-
-
+
+
change <pattern> with <term>
change patt with t
@@ -211,8 +211,8 @@
-
-
+
+
constructor <int>
constructor n
@@ -241,10 +241,10 @@
-
-
+
+
contradiction
- contradiction
+ contradiction
@@ -269,8 +269,8 @@
-
-
+
+
cut <term> [as <id>]
cut P as H
@@ -299,8 +299,8 @@
-
-
+
+
decompose [<ident list>] <ident> [<intros_spec>]
decompose ???
@@ -325,8 +325,8 @@
-
-
+
+
discriminate <term>
discriminate p
@@ -353,8 +353,8 @@ its constructor takes no arguments.
-
-
+
+
elim <term> [using <term>] [<intros_spec>]
elim t using th hyps
@@ -386,8 +386,8 @@ its constructor takes no arguments.
-
-
+
+
elimType <term> [using <term>]
elimType T using th
@@ -412,8 +412,8 @@ its constructor takes no arguments.
-
-
+
+
exact <term>
exact p
@@ -439,10 +439,10 @@ its constructor takes no arguments.
-
-
+
+
exists
- exists
+ exists
@@ -468,9 +468,9 @@ its constructor takes no arguments.
-
-
- fail
+
+
+ fail
fail
@@ -494,8 +494,8 @@ its constructor takes no arguments.
-
-
+
+
fold <reduction_kind> <term> <pattern>
fold red t patt
@@ -525,10 +525,10 @@ its constructor takes no arguments.
-
-
+
+
fourier
- fourier
+ fourier
@@ -554,8 +554,8 @@ its constructor takes no arguments.
-
-
+
+
fwd <ident> [<ident list>]
fwd ...TODO
@@ -580,99 +580,99 @@ its constructor takes no arguments.
-
-
+
+
generalize <pattern> [as <id>]
The tactic generalize
-
-
+
+
id
The tactic id
-
-
+
+
injection <term>
The tactic injection
-
-
+
+
intro [<ident>]
The tactic intro
-
-
+
+
intros <intros_spec>
The tactic intros
-
-
+
+
intros <term>
The tactic intros
-
-
+
+
lapply [depth=<int>] <term> [to <term list] [using <ident>]
The tactic lapply
-
-
+
+
left
The tactic left
-
-
+
+
letin <ident> â <term>
The tactic letin
-
-
+
+
normalize <pattern>
The tactic normalize
-
-
+
+
paramodulation <pattern>
The tactic paramodulation
-
-
+
+
reduce <pattern>
The tactic reduce
-
-
+
+
reflexivity
The tactic reflexivity
-
-
+
+
replace <pattern> with <term>
The tactic replace
-
-
+
+
rewrite {<|>} <term> <pattern>
The tactic rewrite
-
-
+
+
right
The tactic right
-
-
+
+
ring
The tactic ring
-
-
+
+
simplify <pattern>
The tactic simplify
-
-
+
+
split
The tactic split
-
-
+
+
symmetry
The tactic symmetry
-
-
+
+
transitivity <term>
The tactic transitivity
-
-
+
+
unfold [<term>] <pattern>
The tactic unfold
-
-
+
+
whd <pattern>
The tactic whd
-
+
-
+