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