| changeset 10328 | bf33cbd76c05 |
| parent 10281 | 9554ce1c2e54 |
| child 10363 | 6e8002c1790e |
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Wed Oct 25 18:24:33 2000 +0200 @@ -57,6 +57,7 @@ text{*\noindent This time, induction leaves us with the following base case +%{goals[goals_limit=1,display]} \begin{isabelle} \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] \end{isabelle}