--- a/doc-src/IsarRef/Thy/Quick_Reference.thy Wed Mar 04 10:43:39 2009 +0100
+++ b/doc-src/IsarRef/Thy/Quick_Reference.thy Wed Mar 04 10:45:52 2009 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory Quick_Reference
imports Main
begin
@@ -30,7 +28,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"} \\