diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Misc/AdvancedInd.thy
--- 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}