# HG changeset patch # User wenzelm # Date 1234384708 -3600 # Node ID 48634259d41057ea54d127252e98526ddbc81459 # Parent 0cfd533b4e37c478bb11ca7f91db04b74ec33643 proof/qed: optional methods; diff -r 0cfd533b4e37 -r 48634259d410 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\stmt"} & = & @{command "theorem"}~@{text "name: props proof |"}~~@{command "definition"}~@{text "\ | \"} \\[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"} \\