equal
deleted
inserted
replaced
91 \isadelimproof |
91 \isadelimproof |
92 % |
92 % |
93 \endisadelimproof |
93 \endisadelimproof |
94 % |
94 % |
95 \begin{isamarkuptext}% |
95 \begin{isamarkuptext}% |
96 \noindent Single-identifier formulae such as \isa{A} need not |
96 \noindent As you see above, single-identifier formulae such as \isa{A} |
97 be enclosed in double quotes. However, we will continue to do so for |
97 need not be enclosed in double quotes. However, we will continue to do so for |
98 uniformity. |
98 uniformity. |
99 |
99 |
100 Instead of applying fact \isa{a} via the \isa{rule} method, we can |
100 Instead of applying fact \isa{a} via the \isa{rule} method, we can |
101 also push it directly onto our goal. The proof is then immediate, |
101 also push it directly onto our goal. The proof is then immediate, |
102 which is formally written as ``.'' in Isar:% |
102 which is formally written as ``.'' in Isar:% |