X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fdeclarative_tactics_quickref.xml;h=002a7a376bbd4037391b17975ee1ab4e7a01b348;hb=de1ac2d7795925edb488e4fac30d5e80537bfe33;hp=2d09883af5b7647b6218fcf0788a5e6ceb0652ac;hpb=4d23367f20acec9c043c6b81b660ea65ff6f155e;p=helm.git
diff --git a/helm/software/matita/help/C/declarative_tactics_quickref.xml b/helm/software/matita/help/C/declarative_tactics_quickref.xml
index 2d09883af..002a7a376 100644
--- a/helm/software/matita/help/C/declarative_tactics_quickref.xml
+++ b/helm/software/matita/help/C/declarative_tactics_quickref.xml
@@ -5,66 +5,70 @@
&tactic;::=
- we need to proveterm
+ assumeid : sterm|
- we proceed by induction onterm to prove term
+ by induction hypothesis we knowterm (id)|
- assumeid : sterm
+ caseid [(id:term)] ⦠|
- byterm done
+ justificationdone|
- by induction hypothesis we knowterm (id)
+ justificationletid
+ :termsuch thatterm
+ (id)|
- bytermwe provedterm
- (id)
+ [obtainid | concludeterm] =term [auto_params | usingterm | using onceterm | proof] [done]|
- caseid(id:term)
+ supposeterm (id
+ ) [ that is equivalent toterm ]|
- bytermletid
- :termsuch thatterm
- (id)
+ the thesis becomesterm|
- [obtainid | concludeterm] =termby [ term | _ [(auto_params)]] [done]
+ we need to proveterm
+ [(id
+ )]
+ [ or equivalentlyterm]|
- supposeterm (id
- ) [ that is equivalent to term ]
+ we proceed by cases ontermto proveterm|
- the thesis becomessterm
+ we proceed by induction onterm to prove term|
- we proceed by cases on termto proveterm
+ justificationwe provedterm
+ (id
+ )