X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fdeclarative_tactics_quickref.xml;h=002a7a376bbd4037391b17975ee1ab4e7a01b348;hb=f5ca06e7437c022413b14bd8f63fa3466a1ead0c;hp=8aba5a08c16c4a073a9c0bfdb6817e3c6b94049c;hpb=c78a913e4e45c1128b59ca8be9d53fc0c36fc9e0;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 8aba5a08c..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 prove term
+ assume id : sterm
|
- we proceed by induction on term to prove term
+ by induction hypothesis we know term ( id )
|
- assume id : sterm
+ case id [( id : term )] â¦
|
- by term done
+ justification done
|
- by induction hypothesis we know term ( id )
+ justification let id
+ : term such that term
+ ( id )
|
- by term we proved term
- ( id )
+ [obtain id | conclude term] = term [auto_params | using term | using once term | proof] [done]
|
- case id ( id : term )
+ suppose term ( id
+ ) [ that is equivalent to term ]
|
- by term let id
- : term such that term
- ( id )
+ the thesis becomes term
|
- [obtain id | conclude term] = term [auto_params | exact term | using term | proof] [done]
+ we need to prove term
+ [(id
+ )]
+ [ or equivalently term]
|
- suppose term ( id
- ) [ that is equivalent to term ]
+ we proceed by cases on term to prove term
|
- the thesis becomes sterm
+ we proceed by induction on term to prove term
|
- we proceed by cases on term to prove term
+ justification we proved term
+ ( id
+ )