--- a/doc-src/TutorialI/ToyList/ToyList.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu Nov 29 21:12:37 2001 +0100
@@ -142,19 +142,12 @@
@{term"xs"}.
\end{itemize}
The name and the simplification attribute are optional.
-Isabelle's response is to print the initial proof state
-\begin{isabelle}
-proof(prove):~step~0\isanewline
-\isanewline
-goal~(theorem~rev\_rev):\isanewline
-rev~(rev~xs)~=~xs\isanewline
-~1.~rev~(rev~xs)~=~xs
-\end{isabelle}
-The first three lines tell us that we are 0 steps into the proof of
-theorem @{text"rev_rev"}; for compactness reasons we rarely show these
-initial lines in this tutorial. The remaining lines display the current
-\rmindex{proof state}.
-Until we have finished a proof, the proof state always looks like this:
+Isabelle's response is to print the initial proof state consisting
+of some header information (like how many subgoals there are) followed by
+@{goals[display,indent=0]}
+For compactness reasons we omit the header in this tutorial.
+Until we have finished a proof, the \rmindex{proof state} proper
+always looks like this:
\begin{isabelle}
$G$\isanewline
~1.~$G\sb{1}$\isanewline
@@ -165,7 +158,7 @@
is the overall goal that we are trying to prove, and the numbered lines
contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
establish $G$.\index{subgoals}
-At @{text"step 0"} there is only one subgoal, which is
+Initially there is only one subgoal, which is
identical with the overall goal. Normally $G$ is constant and only serves as
a reminder. Hence we rarely show it in this tutorial.