X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Ftactic_quickref.xml;h=e1ff24b3803d82e41e90f20b87873659d4d8c129;hb=01001c883a8151edba81cd03a6f254d24a81c867;hp=58fd32afd506fb8fd67f87f80b9ddc3e0f2010a0;hpb=8752fac73a864c821b6954f0572bce2052924183;p=helm.git
diff --git a/helm/software/matita/help/C/tactic_quickref.xml b/helm/software/matita/help/C/tactic_quickref.xml
index 58fd32afd..e1ff24b38 100644
--- a/helm/software/matita/help/C/tactic_quickref.xml
+++ b/helm/software/matita/help/C/tactic_quickref.xml
@@ -1,206 +1,6 @@
-
-
- absurd sterm
-
-
- apply 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
-
-
-
-
- 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 [as id [id]â¦]
-
-
- generalize pattern [as id]
-
-
-
-
- id
-
-
-
-
- injection sterm
-
-
- intro [id]
-
-
- intros intros-spec
-
-
- inversion sterm
-
-
-
- lapply
- [linear]
- [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
-
-
+
+ tacticssec__tactics
+
+
+
+