X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fhelp%2FC%2Ftactics_quickref.xml;h=6da96f66d1fc1852e577a381680d19f3a87d932d;hb=4361c5423d10853505f47e6b2794a54a211a0b44;hp=12e450fdf49da7e988b91a4790a25f50eb9e7043;hpb=94188b0cbaff6340464d90cc13ee246ea7ec3284;p=helm.git
diff --git a/matita/matita/help/C/tactics_quickref.xml b/matita/matita/help/C/tactics_quickref.xml
index 12e450fdf..6da96f66d 100644
--- a/matita/matita/help/C/tactics_quickref.xml
+++ b/matita/matita/help/C/tactics_quickref.xml
@@ -5,115 +5,97 @@
&tactic;
::=
-
-
- #
-
-
- id
-
-
+ @ sterm
|
-
-
- ##
-
-
+ applyS sterm auto_params
|
-
- #_
+
+ assumption
|
- % [nat] [{stermâ¦}]
-
-
-
- |
-
- *
- [as id]
-
+ /auto_params/.
|
- -id
+ cases
+ term pattern
|
- /auto_params/.
-
-
-
- |
- [<|>] sterm pattern
+ change pattern with sterm
|
- @ sterm
+
+ -id
+
|
- applyS sterm auto_params
+ % [nat] [{stermâ¦}]
|
-
-
- assumption
-
-
+ cut sterm
|
- cases
- term pattern
+ *
+ [as id]
|
- change pattern with sterm
+ destruct
+ [(idâ¦)] [skip (idâ¦)]
|
- cut sterm
+ elim sterm pattern
|
- destruct
- [(idâ¦)] [skip (idâ¦)]
+ generalize pattern
|
- elim sterm pattern
+
+ #
+
+ id
+
+
|
- generalize pattern
+
+ #_
+
@@ -133,12 +115,24 @@
|
letin id â sterm
+
+
+ |
+
+ ##
+
+
|
normalize pattern
[nodelta]
+
+
+ |
+ [<|>] sterm pattern
+
|