X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Ftactics_quickref.xml;h=6da96f66d1fc1852e577a381680d19f3a87d932d;hb=632dfd0a57c9951d0efbd769d6f433c4ef68a314;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..6da96f66d 100644
--- a/matita/matita/help/C/tactics_quickref.xml
+++ b/matita/matita/help/C/tactics_quickref.xml
@@ -5,12 +5,7 @@
&tactic;
::=
- absurd sterm
-
-
-
- |
- apply sterm
+ @ sterm
@@ -29,14 +24,14 @@
|
- auto auto_params. autobatch auto_params
+ /auto_params/.
|
cases
- term pattern [([id]â¦)]
+ term pattern
@@ -48,133 +43,60 @@
|
- clear
- id [idâ¦]
+ -id
|
- clearbody id
-
-
-
- |
- compose [nat] sterm [with sterm] [intros-spec]
+ % [nat] [{stermâ¦}]
|
- constructor nat
+ cut sterm
|
-
- contradiction
-
-
-
-
-
- |
- cut sterm [as id]
-
-
-
- |
-
- decompose
- [as idâ¦]
+ *
+ [as id]
|
- demodulate auto_params
-
-
-
- |
- destruct sterm
-
-
-
- |
- elim sterm pattern [using sterm] intros-spec
-
-
-
- |
- elimType sterm [using sterm] intros-spec
+ destruct
+ [(idâ¦)] [skip (idâ¦)]
|
- exact sterm
+ elim sterm pattern
|
-
-
- exists
-
-
+ generalize pattern
|
-
- fail
-
+ #
+
+ id
+
-
-
- |
- fold reduction-kind sterm pattern
-
|
-
- fourier
-
+ #_
-
-
- |
- fwd id [as id [id]â¦]
-
-
-
- |
- generalize pattern [as id]
-
-
-
- |
-
-
- id
-
-
-
-
-
- |
- intro [id]
-
-
-
- |
- intros intros-spec
-
|
@@ -185,118 +107,36 @@
|
lapply
- [linear]
- [depth=nat]
sterm
- [to
- sterm
- [,stermâ¦]
- ]
- [as id]
-
-
- |
-
-
- left
-
-
-
|
letin id â sterm
-
-
- |
- normalize pattern
-
-
-
- |
-
-
- reflexivity
-
-
-
-
-
- |
- replace pattern with sterm
-
-
-
- |
- rewrite [<|>] sterm pattern
-
-
-
- |
-
-
- right
-
-
-
-
-
- |
-
-
- ring
-
-
-
-
-
- |
- simplify pattern
-
|
-
- split
-
-
-
-
-
- |
-
-
- subst
-
-
-
-
-
- |
-
-
- symmetry
-
+ ##
|
- transitivity sterm
+ normalize pattern
+ [nodelta]
|
- unfold [sterm] pattern
+ [<|>] sterm pattern
|
- whd pattern
+ whd pattern [nodelta]