X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Ftactics_quickref.xml;h=12e450fdf49da7e988b91a4790a25f50eb9e7043;hb=68a413ec8a20ef0d73fcd5810be7db659abe6f92;hp=c7a789c1a32ed246648eb8577e80afb34aa77862;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git
diff --git a/matita/matita/help/C/tactics_quickref.xml b/matita/matita/help/C/tactics_quickref.xml
index c7a789c1a..12e450fdf 100644
--- a/matita/matita/help/C/tactics_quickref.xml
+++ b/matita/matita/help/C/tactics_quickref.xml
@@ -5,175 +5,115 @@
&tactic;
::=
- absurd sterm
-
-
-
- |
- apply sterm
-
-
-
- |
- applyS sterm auto_params
-
-
-
- |
-
- assumption
+
+ #
+
+ id
+
-
-
- |
- auto auto_params. autobatch auto_params
-
-
-
- |
-
- cases
- term pattern [([id]â¦)]
-
-
-
-
- |
- change pattern with sterm
-
|
- clear
- id [idâ¦]
-
-
-
-
- |
- clearbody id
-
-
-
- |
- compose [nat] sterm [with sterm] [intros-spec]
-
-
-
- |
- constructor nat
+
+ ##
+
+
|
-
- contradiction
+
+ #_
|
- cut sterm [as id]
+ % [nat] [{stermâ¦}]
|
- decompose
- [as idâ¦]
+ *
+ [as id]
|
- demodulate auto_params
-
-
-
- |
- destruct sterm
+
+ -id
+
|
- elim sterm pattern [using sterm] intros-spec
+ /auto_params/.
|
- elimType sterm [using sterm] intros-spec
+ [<|>] sterm pattern
|
- exact sterm
+ @ sterm
|
-
-
- exists
-
-
+ applyS sterm auto_params
|
-
- fail
+
+ assumption
-
-
- |
- fold reduction-kind sterm pattern
-
|
-
- fourier
-
-
+ cases
+ term pattern
+
|
- fwd id [as id [id]â¦]
+ change pattern with sterm
|
- generalize pattern [as id]
+ cut sterm
|
-
-
- id
-
-
+ destruct
+ [(idâ¦)] [skip (idâ¦)]
|
- intro [id]
+ elim sterm pattern
|
- intros intros-spec
+ generalize pattern
@@ -185,25 +125,9 @@
|
lapply
- [linear]
- [depth=nat]
sterm
- [to
- sterm
- [,stermâ¦]
- ]
- [as id]
-
-
- |
-
-
- left
-
-
-
|
@@ -212,91 +136,13 @@
|
- normalize pattern
-
-
-
- |
-
-
- reflexivity
-
-
-
-
-
- |
- replace pattern with sterm
-
-
-
- |
- rewrite [<|>] sterm pattern
-
-
-
- |
-
-
- right
-
-
-
-
-
- |
-
-
- ring
-
-
-
-
-
- |
- simplify pattern
-
-
-
- |
-
-
- split
-
-
-
-
-
- |
-
-
- subst
-
-
-
-
-
- |
-
-
- symmetry
-
-
-
-
-
- |
- transitivity sterm
-
-
-
- |
- unfold [sterm] pattern
+ normalize pattern
+ [nodelta]
|
- whd pattern
+ whd pattern [nodelta]