X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Ftactic_quickref.xml;h=e1ff24b3803d82e41e90f20b87873659d4d8c129;hb=f4f44aa85f6d8ad07c44ce5890bd447f04b9c8a2;hp=45e097e1bd1691f7436da434bfd804aef3a7afa0;hpb=cc3ab906b631ef0edb4402cb622fc3fa96682717;p=helm.git
diff --git a/helm/software/matita/help/C/tactic_quickref.xml b/helm/software/matita/help/C/tactic_quickref.xml
index 45e097e1b..e1ff24b38 100644
--- a/helm/software/matita/help/C/tactic_quickref.xml
+++ b/helm/software/matita/help/C/tactic_quickref.xml
@@ -1,201 +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â¦]
-
-
-
- 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 [as 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
-
-
+
+ tacticssec__tactics
+
+
+
+