X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Ftactic_quickref.xml;h=e1ff24b3803d82e41e90f20b87873659d4d8c129;hb=d2a898e8636c360713d8c9967f1de74e3e077c3f;hp=2709769ba91f38b12439ea48465495daf1de079b;hpb=72858765956176eebbd67669db6e2cee8cdb0de0;p=helm.git
diff --git a/helm/software/matita/help/C/tactic_quickref.xml b/helm/software/matita/help/C/tactic_quickref.xml
index 2709769ba..e1ff24b38 100644
--- a/helm/software/matita/help/C/tactic_quickref.xml
+++ b/helm/software/matita/help/C/tactic_quickref.xml
@@ -1,308 +1,6 @@
- tactics
+ tacticssec__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
-
-
-
-
-
- |
- 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
-
-
-
- |
- reduce pattern
-
-
-
- |
-
-
- reflexivity
-
-
-
-
-
- |
- replace pattern with sterm
-
-
-
- |
- rewrite [<|>] sterm pattern
-
-
-
- |
-
-
- right
-
-
-
-
-
- |
-
-
- ring
-
-
-
-
-
- |
- simplify pattern
-
-
-
- |
-
-
- split
-
-
-
-
-
- |
-
-
- subst
-
-
-
-
-
- |
-
-
- symmetry
-
-
-
-
-
- |
- transitivity sterm
-
-
-
- |
- unfold [sterm] pattern
-
-
-
- |
- whd pattern
-
-
+