X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fhelp%2FC%2Ftactics_quickref.xml;fp=matita%2Fhelp%2FC%2Ftactics_quickref.xml;h=331d58dc2902b94461ed3d40d85b2c38d689e663;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1
diff --git a/matita/help/C/tactics_quickref.xml b/matita/help/C/tactics_quickref.xml
new file mode 100644
index 000000000..331d58dc2
--- /dev/null
+++ b/matita/help/C/tactics_quickref.xml
@@ -0,0 +1,303 @@
+
+ tactics
+
+
+
+ &tactic;
+ ::=
+ absurd sterm
+
+
+
+ |
+ apply sterm
+
+
+
+ |
+ applyS sterm auto_params
+
+
+
+ |
+
+
+ assumption
+
+
+
+
+
+ |
+ auto auto_params
+
+
+
+ |
+
+ cases
+ term [([id]â¦)]
+
+
+
+
+ |
+ change pattern with sterm
+
+
+
+ |
+
+ clear
+ id [idâ¦]
+
+
+
+
+ |
+ clearbody id
+
+
+
+ |
+ compose [nat] sterm [with sterm] [intros-spec]
+
+
+
+ |
+ constructor nat
+
+
+
+ |
+
+
+ contradiction
+
+
+
+
+
+ |
+ cut sterm [as id]
+
+
+
+ |
+
+ decompose
+ [as idâ¦]
+
+
+
+
+ |
+ demodulate auto_params
+
+
+
+ |
+ destruct 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
+
+
+
+
+
+ |
+ intro [id]
+
+
+
+ |
+ intros intros-spec
+
+
+
+ |
+ inversion sterm
+
+
+
+ |
+
+ 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
+
+
+
+ |
+ unfold [sterm] pattern
+
+
+
+ |
+ whd pattern
+
+
+
+