X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_declarative_tactics.xml;h=cc6aeb61de2ae497fff42a6b7ad44909d693baf2;hb=ba5c1c83e77e701ef11625687ec27931bc4bb944;hp=b8b8777791660d7dda447dd266b6f0a1b51cc864;hpb=cd425125163b22a968f2ff1da6f80b83c35614b5;p=helm.git
diff --git a/helm/software/matita/help/C/sec_declarative_tactics.xml b/helm/software/matita/help/C/sec_declarative_tactics.xml
index b8b877779..cc6aeb61d 100644
--- a/helm/software/matita/help/C/sec_declarative_tactics.xml
+++ b/helm/software/matita/help/C/sec_declarative_tactics.xml
@@ -67,13 +67,13 @@
Pre-condition:
- Da Fare
+ &TODO;
Action:
- Da Fare
+ &TODO;
@@ -135,13 +135,13 @@
Pre-condition:
- Da Fare
+ &TODO;
Action:
- Da Fare
+ &TODO;
@@ -203,13 +203,13 @@
Pre-condition:
- Da Fare
+ &TODO;
Action:
- Da Fare
+ &TODO;
@@ -237,13 +237,13 @@
Pre-condition:
- Da Fare
+ &TODO;
Action:
- Da Fare
+ &TODO;
@@ -305,19 +305,19 @@
Pre-condition:
- Da Fare
+ &TODO;
Action:
- Da Fare
+ &TODO;
New sequents to prove:
- Da Fare
+ &TODO;
@@ -327,31 +327,31 @@
obtain/conclude
obtain/conclude
- obtain H t=t by [t|_] done
+ obtain H t=t [auto_params | exact t| proof | using t] done
Synopsis:
- [obtain &id; | conclude &term;] = &term; by [ &term; | _ [(&autoparams;)]] [done]
+ [obtain &id; | conclude &term;] = &term; [&autoparams; | exact &term; | using &term; | proof] [done]
Pre-condition:
- Da Fare
+ &TODO;
Action:
- Da Fare
+ &TODO;
New sequence to prove:
- Da Fare
+ &TODO;
@@ -387,7 +387,7 @@
New sequence to prove:
- Da fare
+ &TODO;