proof/qed: optional methods;
authorwenzelm
Wed, 11 Feb 2009 21:38:28 +0100
changeset 29724 48634259d410
parent 29723 0cfd533b4e37
child 29725 03916d2d16d3
proof/qed: optional methods;
doc-src/IsarRef/Thy/Quick_Reference.thy
--- a/doc-src/IsarRef/Thy/Quick_Reference.thy	Wed Feb 11 21:38:03 2009 +0100
+++ b/doc-src/IsarRef/Thy/Quick_Reference.thy	Wed Feb 11 21:38:28 2009 +0100
@@ -30,7 +30,7 @@
 
   \begin{tabular}{rcl}
     @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: props proof  |"}~~@{command "definition"}~@{text "\<dots>  |  \<dots>"} \\[1ex]
-    @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method stmt\<^sup>*"}~@{command "qed"}~@{text method} \\
+    @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\
     & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex]
     @{text prfx} & = & @{command "apply"}~@{text method} \\
     & @{text "|"} & @{command "using"}~@{text "facts"} \\