equal
deleted
inserted
replaced
204 \noindent |
204 \noindent |
205 Typically, we begin by unfolding some definitions: |
205 Typically, we begin by unfolding some definitions: |
206 \indexbold{definitions!unfolding}% |
206 \indexbold{definitions!unfolding}% |
207 \end{isamarkuptxt}% |
207 \end{isamarkuptxt}% |
208 \isamarkuptrue% |
208 \isamarkuptrue% |
209 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
209 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
210 % |
210 % |
211 \begin{isamarkuptxt}% |
211 \begin{isamarkuptxt}% |
212 \noindent |
212 \noindent |
213 In this particular case, the resulting goal |
213 In this particular case, the resulting goal |
214 \begin{isabelle}% |
214 \begin{isabelle}% |