47 \mbox{\isa{\isacommand{note}}}~\isa{a\ {\isacharequal}\ b} & reconsider facts \\ |
47 \mbox{\isa{\isacommand{note}}}~\isa{a\ {\isacharequal}\ b} & reconsider facts \\ |
48 \mbox{\isa{\isacommand{let}}}~\isa{p\ {\isacharequal}\ t} & abbreviate terms by higher-order matching \\ |
48 \mbox{\isa{\isacommand{let}}}~\isa{p\ {\isacharequal}\ t} & abbreviate terms by higher-order matching \\ |
49 \end{tabular} |
49 \end{tabular} |
50 |
50 |
51 \begin{matharray}{rcl} |
51 \begin{matharray}{rcl} |
52 \isa{theory{\isasymdash}stmt} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{name{\isacharcolon}\ prop\ proof} \Or \mbox{\isa{\isacommand{definition}}}~\dots \Or \dots \\[1ex] |
52 \isa{theory{\isasymdash}stmt} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{name{\isacharcolon}\ props\ proof} \Or \mbox{\isa{\isacommand{definition}}}~\dots \Or \dots \\[1ex] |
53 \isa{proof} & = & \isa{prfx\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{proof}}}~\isa{method\ stmt\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{qed}}}~\isa{method} \\ |
53 \isa{proof} & = & \isa{prfx\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{proof}}}~\isa{method\ stmt\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{qed}}}~\isa{method} \\ |
54 & \Or & \isa{prfx\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{done}}} \\[1ex] |
54 & \Or & \isa{prfx\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{done}}} \\[1ex] |
55 \isa{prfx} & = & \mbox{\isa{\isacommand{apply}}}~\isa{method} \\ |
55 \isa{prfx} & = & \mbox{\isa{\isacommand{apply}}}~\isa{method} \\ |
56 & \Or & \mbox{\isa{\isacommand{using}}}~\isa{name\isactrlsup {\isacharplus}} \\ |
56 & \Or & \mbox{\isa{\isacommand{using}}}~\isa{facts} \\ |
57 & \Or & \mbox{\isa{\isacommand{unfolding}}}~\isa{name\isactrlsup {\isacharplus}} \\ |
57 & \Or & \mbox{\isa{\isacommand{unfolding}}}~\isa{facts} \\ |
58 \isa{stmt} & = & \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{stmt\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} \\ |
58 \isa{stmt} & = & \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{stmt\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} \\ |
59 & \Or & \mbox{\isa{\isacommand{next}}} \\ |
59 & \Or & \mbox{\isa{\isacommand{next}}} \\ |
60 & \Or & \mbox{\isa{\isacommand{note}}}~\isa{name\ {\isacharequal}\ name\isactrlsup {\isacharplus}} \\ |
60 & \Or & \mbox{\isa{\isacommand{note}}}~\isa{name\ {\isacharequal}\ facts} \\ |
61 & \Or & \mbox{\isa{\isacommand{let}}}~\isa{term\ {\isacharequal}\ term} \\ |
61 & \Or & \mbox{\isa{\isacommand{let}}}~\isa{term\ {\isacharequal}\ term} \\ |
62 & \Or & \mbox{\isa{\isacommand{fix}}}~\isa{var\isactrlsup {\isacharplus}} \\ |
62 & \Or & \mbox{\isa{\isacommand{fix}}}~\isa{var\isactrlsup {\isacharplus}} \\ |
63 & \Or & \mbox{\isa{\isacommand{assume}}}~\isa{name{\isacharcolon}\ prop\isactrlsup {\isacharplus}} \\ |
63 & \Or & \mbox{\isa{\isacommand{assume}}}~\isa{name{\isacharcolon}\ props} \\ |
64 & \Or & \mbox{\isa{\isacommand{then}}}\isa{\isactrlsup {\isacharquery}}~\isa{goal} \\ |
64 & \Or & \mbox{\isa{\isacommand{then}}}\isa{\isactrlsup {\isacharquery}}~\isa{goal} \\ |
65 \isa{goal} & = & \mbox{\isa{\isacommand{have}}}~\isa{name{\isacharcolon}\ prop\isactrlsup {\isacharplus}\ proof} \\ |
65 \isa{goal} & = & \mbox{\isa{\isacommand{have}}}~\isa{name{\isacharcolon}\ props\ proof} \\ |
66 & \Or & \mbox{\isa{\isacommand{show}}}~\isa{name{\isacharcolon}\ prop\isactrlsup {\isacharplus}\ proof} \\ |
66 & \Or & \mbox{\isa{\isacommand{show}}}~\isa{name{\isacharcolon}\ props\ proof} \\ |
67 \end{matharray}% |
67 \end{matharray}% |
68 \end{isamarkuptext}% |
68 \end{isamarkuptext}% |
69 \isamarkuptrue% |
69 \isamarkuptrue% |
70 % |
70 % |
71 \isamarkupsubsection{Abbreviations and synonyms% |
71 \isamarkupsubsection{Abbreviations and synonyms% |