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