equal
deleted
inserted
replaced
354 \begin{isabelle} |
354 \begin{isabelle} |
355 \isacommand{thm}~@{thm [source] test}\\ |
355 \isacommand{thm}~@{thm [source] test}\\ |
356 @{text ">"}~@{thm test} |
356 @{text ">"}~@{thm test} |
357 \end{isabelle} |
357 \end{isabelle} |
358 |
358 |
|
359 As can be seen, the schematic variable @{text "?X"} has been instantiated inside the proof. |
|
360 |
359 \begin{readmore} |
361 \begin{readmore} |
360 For more information about the internals of goals see \isccite{sec:tactical-goals}. |
362 For more information about the internals of goals see \isccite{sec:tactical-goals}. |
361 \end{readmore} |
363 \end{readmore} |
362 |
364 |
363 *} |
365 *} |