equal
deleted
inserted
replaced
28 |
28 |
29 \medskip |
29 \medskip |
30 |
30 |
31 \begin{tabular}{rcl} |
31 \begin{tabular}{rcl} |
32 @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: props proof |"}~~@{command "definition"}~@{text "\<dots> | \<dots>"} \\[1ex] |
32 @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: props proof |"}~~@{command "definition"}~@{text "\<dots> | \<dots>"} \\[1ex] |
33 @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method stmt\<^sup>*"}~@{command "qed"}~@{text method} \\ |
33 @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\ |
34 & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex] |
34 & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex] |
35 @{text prfx} & = & @{command "apply"}~@{text method} \\ |
35 @{text prfx} & = & @{command "apply"}~@{text method} \\ |
36 & @{text "|"} & @{command "using"}~@{text "facts"} \\ |
36 & @{text "|"} & @{command "using"}~@{text "facts"} \\ |
37 & @{text "|"} & @{command "unfolding"}~@{text "facts"} \\ |
37 & @{text "|"} & @{command "unfolding"}~@{text "facts"} \\ |
38 @{text stmt} & = & @{command "{"}~@{text "stmt\<^sup>*"}~@{command "}"} \\ |
38 @{text stmt} & = & @{command "{"}~@{text "stmt\<^sup>*"}~@{command "}"} \\ |