X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Ftactic_quickref.xml;h=e1ff24b3803d82e41e90f20b87873659d4d8c129;hb=2d2add82882aa070af5d942ebf5b7fa43359e1fd;hp=6a735eee247779b3bb19494190ebb2c3e556b92c;hpb=a713b1508a5eaa20d1a2051366e3ec6057b7693b;p=helm.git
diff --git a/helm/software/matita/help/C/tactic_quickref.xml b/helm/software/matita/help/C/tactic_quickref.xml
index 6a735eee2..e1ff24b38 100644
--- a/helm/software/matita/help/C/tactic_quickref.xml
+++ b/helm/software/matita/help/C/tactic_quickref.xml
@@ -1,186 +1,6 @@
-
-
- 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 [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
+
+
+
+