
diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Oct 25 17:44:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Oct 25 18:24:33 2000 +0200
@@ -54,6 +54,7 @@
 \begin{isamarkuptext}%
 \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}




