X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fdeclarative_tactics_quickref.xml;h=79ab7a5348b32377598faf4e50a34aee02c7f9c2;hb=d29fd4947ea4551f1fa078e56ed2a21b4515536f;hp=1f16a47251d8032b2f38568f6d0d0bea541b8ea4;hpb=a19551fd50df93951d78eea4c163d434f844047c;p=helm.git
diff --git a/matita/matita/help/C/declarative_tactics_quickref.xml b/matita/matita/help/C/declarative_tactics_quickref.xml
index 1f16a4725..79ab7a534 100644
--- a/matita/matita/help/C/declarative_tactics_quickref.xml
+++ b/matita/matita/help/C/declarative_tactics_quickref.xml
@@ -1,6 +1,101 @@
tactics
-
+
+
+ &tactic;
+ ::=
+
+ = term [auto_params | using term | using once term | proof] [done]
+
+
+
+
+ |
+ assume id :
+ sterm
+
+
+
+ |
+ by induction hypothesis we know term ( id )
+
+
+
+ |
+ case id [( id : term )] ⦠[( id : term )]
+
+
+
+ |
+ conclude term
+
+
+
+ |
+ justification done
+
+
+
+ |
+ justification let id
+ : term such that term
+ ( id )
+
+
+
+ |
+ let id = term
+
+
+
+ |
+ obtain id term
+
+
+
+ |
+ suppose term ( id
+ )
+
+
+
+ |
+
+ that is equivalent to term
+
+
+
+
+ |
+ the thesis becomes term
+
+
+
+ |
+ we need to prove term
+ [(id
+ )]
+
+
+
+
+ |
+ we proceed by cases on term to prove term
+
+
+
+ |
+ we proceed by induction on term to prove term
+
+
+
+ |
+ justification we proved term
+ [( id
+ )]
+
+
+