X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Ftactic_quickref.xml;h=1549d3794a3b9e298afeca205f9e9f44ecbb7fb4;hb=69c5a60dfa385a3d0e270ed38eb0d970366792c5;hp=e1f7eb434e1c530e1bef0f22fc0a38e1356bd10a;hpb=522d835109b6df16e1c082ae128c0e08677cbb1b;p=helm.git
diff --git a/helm/software/matita/help/C/tactic_quickref.xml b/helm/software/matita/help/C/tactic_quickref.xml
index e1f7eb434..1549d3794 100644
--- a/helm/software/matita/help/C/tactic_quickref.xml
+++ b/helm/software/matita/help/C/tactic_quickref.xml
@@ -1,182 +1,303 @@
-
-
- absurd sterm
-
-
- apply sterm
-
-
-
-
- assumption
-
-
-
-
- auto [depth=nat] [width=nat] [paramodulation] [full]
-
-
- change pattern with sterm
-
-
- clear id
-
-
- clearbody id
-
-
- constructor nat
-
-
-
-
- contradiction
-
-
-
-
- cut sterm [as id]
-
-
- decompose id [id]⦠intros-spec
-
-
- demodulation pattern
-
-
- discriminate sterm
-
-
- elim sterm [using sterm] intros-spec
-
-
- elimType sterm [using sterm] intros-spec
-
-
- exact sterm
-
-
-
-
- exists
-
-
-
-
-
-
- fail
-
-
-
-
- fold reduction-kind sterm pattern
-
-
-
-
- fourier
-
-
-
-
- fwd id [([id]â¦)]
-
-
- generalize pattern [as id]
-
-
-
-
- id
-
-
-
-
- injection sterm
-
-
- intro [id]
-
-
- intros intros-spec
-
-
- inversion sterm
-
-
- lapply [depth=nat] sterm [to sterm [sterm]â¦] [as id]
-
-
-
-
- left
-
-
-
-
- letin id â sterm
-
-
- normalize pattern
-
-
- paramodulation pattern
-
-
- reduce pattern
-
-
-
-
- reflexivity
-
-
-
-
- replace pattern with sterm
-
-
- rewrite [<|>] sterm pattern
-
-
-
-
- right
-
-
-
-
-
-
- ring
-
-
-
-
- simplify pattern
-
-
-
-
- split
-
-
-
-
-
-
- symmetry
-
-
-
-
- transitivity sterm
-
-
- unfold [sterm] pattern
-
-
- whd pattern
-
-
+
+ tactics
+
+
+
+ &tactic;
+ ::=
+ absurd sterm
+
+
+
+ |
+ apply sterm
+
+
+
+ |
+ applyS sterm
+
+
+
+ |
+
+
+ assumption
+
+
+
+
+
+ |
+ auto [depth=nat] [width=nat] [paramodulation] [full]
+
+
+
+ |
+ change pattern with sterm
+
+
+
+ |
+
+ clear
+ id [idâ¦]
+
+
+
+
+ |
+ clearbody id
+
+
+
+ |
+ constructor nat
+
+
+
+ |
+
+
+ contradiction
+
+
+
+
+
+ |
+ cut sterm [as id]
+
+
+
+ |
+
+ decompose
+ [(
+ idâ¦
+ )]
+ [id]
+ [as idâ¦]
+
+
+
+
+ |
+
+
+ demodulate
+
+
+
+
+
+ |
+ destruct sterm
+
+
+
+ |
+ elim sterm [using sterm] intros-spec
+
+
+
+ |
+ elimType sterm [using sterm] intros-spec
+
+
+
+ |
+ exact sterm
+
+
+
+ |
+
+
+ exists
+
+
+
+
+
+ |
+
+
+ fail
+
+
+
+
+
+ |
+ fold reduction-kind sterm pattern
+
+
+
+ |
+
+
+ fourier
+
+
+
+
+
+ |
+ fwd id [as id [id]â¦]
+
+
+
+ |
+ generalize pattern [as id]
+
+
+
+ |
+
+
+ id
+
+
+
+
+
+ |
+ intro [id]
+
+
+
+ |
+ intros intros-spec
+
+
+
+ |
+ inversion sterm
+
+
+
+ |
+
+ lapply
+ [linear]
+ [depth=nat]
+ sterm
+ [to
+ sterm
+ [,stermâ¦]
+ ]
+ [as id]
+
+
+
+
+ |
+
+
+ left
+
+
+
+
+
+ |
+ letin id â sterm
+
+
+
+ |
+ normalize pattern
+
+
+
+ |
+ reduce pattern
+
+
+
+ |
+
+
+ reflexivity
+
+
+
+
+
+ |
+ replace pattern with sterm
+
+
+
+ |
+ rewrite [<|>] sterm pattern
+
+
+
+ |
+
+
+ right
+
+
+
+
+
+ |
+
+
+ ring
+
+
+
+
+
+ |
+ simplify pattern
+
+
+
+ |
+
+
+ split
+
+
+
+
+
+ |
+
+
+ subst
+
+
+
+
+
+ |
+
+
+ symmetry
+
+
+
+
+
+ |
+ transitivity sterm
+
+
+
+ |
+ unfold [sterm] pattern
+
+
+
+ |
+ whd pattern
+
+
+
+