X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fdeclarative_tactics_quickref.xml;h=8aba5a08c16c4a073a9c0bfdb6817e3c6b94049c;hb=4108cbe1ef492c92cc6c7576e9c4148760637eaf;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..8aba5a08c 100644
--- a/helm/software/matita/help/C/declarative_tactics_quickref.xml
+++ b/helm/software/matita/help/C/declarative_tactics_quickref.xml
@@ -48,7 +48,7 @@
|
- [obtain id | conclude term] = term by [ term | _ [(auto_params)]] [done]
+ [obtain id | conclude term] = term [auto_params | exact term | using term | proof] [done]