# HG changeset patch
# User nipkow
# Date 972978792 -3600
# Node ID c6b197ccf1f120d79d13ae65de23c158e0b2889b
# Parent  c20f78a9606f5d569f1ceeda9d1c504eae55bdcc
*** empty log message ***

diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/CTL/Base.thy
--- a/doc-src/TutorialI/CTL/Base.thy	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/CTL/Base.thy	Tue Oct 31 08:53:12 2000 +0100
@@ -2,7 +2,7 @@
 
 section{*Case study: Verified model checking*}
 
-text{*
+text{*\label{sec:VMC}
 Model checking is a very popular technique for the verification of finite
 state systems (implementations) w.r.t.\ temporal logic formulae
 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Tue Oct 31 08:53:12 2000 +0100
@@ -5,6 +5,7 @@
 \isamarkupsection{Case study: Verified model checking}
 %
 \begin{isamarkuptext}%
+\label{sec:VMC}
 Model checking is a very popular technique for the verification of finite
 state systems (implementations) w.r.t.\ temporal logic formulae
 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/IsaMakefile	Tue Oct 31 08:53:12 2000 +0100
@@ -142,7 +142,7 @@
 
 HOL-Types: HOL $(LOG)/HOL-Types.gz
 
-$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
+$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML Types/Typedef.thy \
   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
   Types/Overloading.thy Types/Axioms.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Tue Oct 31 08:53:12 2000 +0100
@@ -35,7 +35,7 @@
 gradually, using only @{text"#"}:
 *}
 
-consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
+consts itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list";
 primrec
 "itrev []     ys = ys"
 "itrev (x#xs) ys = itrev xs (x#ys)";
@@ -75,7 +75,7 @@
 *};
 (*<*)oops;(*>*)
 lemma "itrev xs ys = rev xs @ ys";
-
+(*<*)apply(induct_tac xs, simp_all)(*>*)
 txt{*\noindent
 If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
 @{term"rev xs"}, just as required.
@@ -87,11 +87,7 @@
 Although we now have two variables, only @{term"xs"} is suitable for
 induction, and we repeat our above proof attempt. Unfortunately, we are still
 not there:
-\begin{isabelle}\makeatother
-~1.~{\isasymAnd}a~list.\isanewline
-~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
-~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
-\end{isabelle}
+@{subgoals[display,indent=0,goals_limit=1]}
 The induction hypothesis is still too weak, but this time it takes no
 intuition to generalize: the problem is that @{term"ys"} is fixed throughout
 the subgoal, but the induction hypothesis needs to be applied with
@@ -99,7 +95,7 @@
 for all @{term"ys"} instead of a fixed one:
 *};
 (*<*)oops;(*>*)
-lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
+lemma "\<forall>ys. itrev xs ys = rev xs @ ys";
 (*<*)
 by(induct_tac xs, simp_all);
 (*>*)
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Misc/document/Itrev.tex
--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Tue Oct 31 08:53:12 2000 +0100
@@ -84,10 +84,10 @@
 Although we now have two variables, only \isa{xs} is suitable for
 induction, and we repeat our above proof attempt. Unfortunately, we are still
 not there:
-\begin{isabelle}\makeatother
-~1.~{\isasymAnd}a~list.\isanewline
-~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
-~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
+\ \ \ \ \ \ \ itrev\ list\ ys\ {\isacharequal}\ rev\ list\ {\isacharat}\ ys\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ \ \ itrev\ list\ {\isacharparenleft}a\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ ys%
 \end{isabelle}
 The induction hypothesis is still too weak, but this time it takes no
 intuition to generalize: the problem is that \isa{ys} is fixed throughout
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Tue Oct 31 08:53:12 2000 +0100
@@ -151,8 +151,8 @@
 \begin{isamarkuptxt}%
 \noindent
 In this particular case, the resulting goal
-\begin{isabelle}
-~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ A\ {\isasymand}\ {\isasymnot}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ A\ {\isasymand}\ {\isasymnot}\ A%
 \end{isabelle}
 can be proved by simplification. Thus we could have proved the lemma outright by%
 \end{isamarkuptxt}%
@@ -227,15 +227,14 @@
 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
-can be split into
-\begin{isabelle}
-~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
-\end{isabelle}
-by a degenerate form of simplification%
+can be split by a degenerate form of simplification%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
-\begin{isamarkuptext}%
+\begin{isamarkuptxt}%
 \noindent
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymforall}xs{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}%
+\end{isabelle}
 where no simplification rules are included (\isa{only{\isacharcolon}} is followed by the
 empty list of theorems) but the rule \isaindexbold{split_if} for
 splitting \isa{if}s is added (via the modifier \isa{split{\isacharcolon}}). Because
@@ -244,25 +243,20 @@
 on the initial goal above.
 
 This splitting idea generalizes from \isa{if} to \isaindex{case}:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}%
+\end{isamarkuptxt}%
+\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
 \begin{isamarkuptxt}%
-\noindent
-becomes
-\begin{isabelle}\makeatother
-~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
-~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}\ {\isasymand}\isanewline
+\ \ \ \ {\isacharparenleft}{\isasymforall}a\ list{\isachardot}\ xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymlongrightarrow}\ a\ {\isacharhash}\ list\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}%
 \end{isabelle}
-by typing%
-\end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
 In contrast to \isa{if}-expressions, the simplifier does not split
 \isa{case}-expressions by default because this can lead to nontermination
 in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is
 dropped, the above goal is solved,%
-\end{isamarkuptext}%
+\end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent%
@@ -292,13 +286,13 @@
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
-\begin{isamarkuptext}%
+\begin{isamarkuptxt}%
 \noindent
 In contrast to splitting the conclusion, this actually creates two
 separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}):
-\begin{isabelle}
-\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
-\ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}%
 \end{isabelle}
 If you need to split both in the assumptions and the conclusion,
 use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
@@ -314,7 +308,7 @@
 \end{warn}
 
 \index{*split|)}%
-\end{isamarkuptext}%
+\end{isamarkuptxt}%
 %
 \isamarkupsubsubsection{Arithmetic}
 %
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Tue Oct 31 08:53:12 2000 +0100
@@ -154,9 +154,7 @@
 
 txt{*\noindent
 In this particular case, the resulting goal
-\begin{isabelle}
-~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
-\end{isabelle}
+@{subgoals[display,indent=0]}
 can be proved by simplification. Thus we could have proved the lemma outright by
 *}(*<*)oops;lemma "exor A (\<not>A)";(*>*)
 apply(simp add: exor_def)
@@ -237,17 +235,13 @@
 lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
 
 txt{*\noindent
-can be split into
-\begin{isabelle}
-~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
-\end{isabelle}
-by a degenerate form of simplification
+can be split by a degenerate form of simplification
 *}
 
 apply(simp only: split: split_if);
-(*<*)oops;(*>*)
 
-text{*\noindent
+txt{*\noindent
+@{subgoals[display,indent=0]}
 where no simplification rules are included (@{text"only:"} is followed by the
 empty list of theorems) but the rule \isaindexbold{split_if} for
 splitting @{text"if"}s is added (via the modifier @{text"split:"}). Because
@@ -256,28 +250,19 @@
 on the initial goal above.
 
 This splitting idea generalizes from @{text"if"} to \isaindex{case}:
-*}
+*}(*<*)oops;(*>*)
 
 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
-txt{*\noindent
-becomes
-\begin{isabelle}\makeatother
-~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
-~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
-\end{isabelle}
-by typing
-*}
+apply(simp only: split: list.split);
 
-apply(simp only: split: list.split);
-(*<*)oops;(*>*)
-
-text{*\noindent
+txt{*
+@{subgoals[display,indent=0]}
 In contrast to @{text"if"}-expressions, the simplifier does not split
 @{text"case"}-expressions by default because this can lead to nontermination
 in case of recursive datatypes. Again, if the @{text"only:"} modifier is
 dropped, the above goal is solved,
 *}
-(*<*)
+(*<*)oops;
 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
 (*>*)
 apply(simp split: list.split);
@@ -317,17 +302,11 @@
 
 lemma "if xs = [] then ys ~= [] else ys = [] ==> xs @ ys ~= []"
 apply(simp only: split: split_if_asm);
-(*<*)
-by(simp_all)
-(*>*)
 
-text{*\noindent
+txt{*\noindent
 In contrast to splitting the conclusion, this actually creates two
 separate subgoals (which are solved by @{text"simp_all"}):
-\begin{isabelle}
-\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
-\ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
-\end{isabelle}
+@{subgoals[display,indent=0]}
 If you need to split both in the assumptions and the conclusion,
 use $t$@{text".splits"} which subsumes $t$@{text".split"} and
 $t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}.
@@ -343,6 +322,9 @@
 
 \index{*split|)}
 *}
+(*<*)
+by(simp_all)
+(*>*)
 
 
 subsubsection{*Arithmetic*}
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Recdef/Induction.thy
--- a/doc-src/TutorialI/Recdef/Induction.thy	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Recdef/Induction.thy	Tue Oct 31 08:53:12 2000 +0100
@@ -31,13 +31,7 @@
 txt{*\noindent
 The resulting proof state has three subgoals corresponding to the three
 clauses for @{term"sep"}:
-\begin{isabelle}
-~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
-~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
-~3.~{\isasymAnd}a~x~y~zs.\isanewline
-~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
-~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
-\end{isabelle}
+@{subgoals[display,indent=0]}
 The rest is pure simplification:
 *}
 
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Recdef/document/Induction.tex
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Oct 31 08:53:12 2000 +0100
@@ -29,12 +29,12 @@
 \noindent
 The resulting proof state has three subgoals corresponding to the three
 clauses for \isa{sep}:
-\begin{isabelle}
-~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
-~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
-~3.~{\isasymAnd}a~x~y~zs.\isanewline
-~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
-~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ x{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\isanewline
+\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ x\ y\ zs{\isachardot}\isanewline
+\ \ \ \ \ \ \ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ \ \ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}%
 \end{isabelle}
 The rest is pure simplification:%
 \end{isamarkuptxt}%
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Recdef/document/examples.tex
--- a/doc-src/TutorialI/Recdef/document/examples.tex	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Tue Oct 31 08:53:12 2000 +0100
@@ -64,7 +64,7 @@
 \end{isamarkuptext}%
 \isacommand{consts}\ sep{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
 \isacommand{recdef}\ sep{\isadigit{2}}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}sep{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{2}}\ zs\ a{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{2}}\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}\ a{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ {\isachardoublequote}sep{\isadigit{2}}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 Because of its pattern-matching syntax, \isacommand{recdef} is also useful
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Recdef/examples.thy
--- a/doc-src/TutorialI/Recdef/examples.thy	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Recdef/examples.thy	Tue Oct 31 08:53:12 2000 +0100
@@ -69,7 +69,7 @@
 *}
 consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
 recdef sep2 "measure length"
-  "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 zs a)"
+  "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 (y#zs) a)"
   "sep2 xs       = (\<lambda>a. xs)";
 
 text{*
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Oct 31 08:53:12 2000 +0100
@@ -248,13 +248,10 @@
 apply(auto);
 
 txt{*
-\begin{isabelle}
-~1.~rev~ys~=~rev~ys~@~[]\isanewline
-~2. \dots
-\end{isabelle}
-Again, we need to abandon this proof attempt and prove another simple lemma first.
-In the future the step of abandoning an incomplete proof before embarking on
-the proof of a lemma usually remains implicit.
+@{subgoals[display,indent=0,goals_limit=1]}
+Again, we need to abandon this proof attempt and prove another simple lemma
+first. In the future the step of abandoning an incomplete proof before
+embarking on the proof of a lemma usually remains implicit.
 *}
 (*<*)
 oops
@@ -273,11 +270,7 @@
 txt{*
 \noindent
 leads to the desired message @{text"No subgoals!"}:
-\begin{isabelle}
-xs~@~[]~=~xs\isanewline
-No~subgoals!
-\end{isabelle}
-
+@{goals[display,indent=0]}
 We still need to confirm that the proof is now finished:
 *}
 
@@ -306,11 +299,7 @@
 \noindent
 we find that this time @{text"auto"} solves the base case, but the
 induction step merely simplifies to
-\begin{isabelle}
-~1.~{\isasymAnd}a~list.\isanewline
-~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
-~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
-\end{isabelle}
+@{subgoals[display,indent=0,goals_limit=1]}
 Now we need to remember that @{text"@"} associates to the right, and that
 @{text"#"} and @{text"@"} have the same priority (namely the @{text"65"}
 in their \isacommand{infixr} annotation). Thus the conclusion really is
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Oct 31 08:53:12 2000 +0100
@@ -234,13 +234,12 @@
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
 \begin{isamarkuptxt}%
-\begin{isabelle}
-~1.~rev~ys~=~rev~ys~@~[]\isanewline
-~2. \dots
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ rev\ ys\ {\isacharequal}\ rev\ ys\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}%
 \end{isabelle}
-Again, we need to abandon this proof attempt and prove another simple lemma first.
-In the future the step of abandoning an incomplete proof before embarking on
-the proof of a lemma usually remains implicit.%
+Again, we need to abandon this proof attempt and prove another simple lemma
+first. In the future the step of abandoning an incomplete proof before
+embarking on the proof of a lemma usually remains implicit.%
 \end{isamarkuptxt}%
 %
 \isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}}
@@ -254,11 +253,10 @@
 \begin{isamarkuptxt}%
 \noindent
 leads to the desired message \isa{No\ subgoals{\isacharbang}}:
-\begin{isabelle}
-xs~@~[]~=~xs\isanewline
-No~subgoals!
+\begin{isabelle}%
+xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
+No\ subgoals{\isacharbang}%
 \end{isabelle}
-
 We still need to confirm that the proof is now finished:%
 \end{isamarkuptxt}%
 \isacommand{done}%
@@ -284,10 +282,10 @@
 \noindent
 we find that this time \isa{auto} solves the base case, but the
 induction step merely simplifies to
-\begin{isabelle}
-~1.~{\isasymAnd}a~list.\isanewline
-~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
-~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
+\ \ \ \ \ \ \ rev\ {\isacharparenleft}list\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ \ \ {\isacharparenleft}rev\ ys\ {\isacharat}\ rev\ list{\isacharparenright}\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}%
 \end{isabelle}
 Now we need to remember that \isa{{\isacharat}} associates to the right, and that
 \isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}}
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Types/Axioms.thy
--- a/doc-src/TutorialI/Types/Axioms.thy	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Types/Axioms.thy	Tue Oct 31 08:53:12 2000 +0100
@@ -59,7 +59,7 @@
 txt{*\noindent
 This time @{text intro_classes} leaves us with the four axioms,
 specialized to type @{typ bool}, as subgoals:
-@{goals[display,show_types,indent=0]}
+@{subgoals[display,show_types,indent=0]}
 Fortunately, the proof is easy for blast, once we have unfolded the definitions
 of @{text"<<"} and @{text"<<="} at @{typ bool}:
 *}
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Types/ROOT.ML
--- a/doc-src/TutorialI/Types/ROOT.ML	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Types/ROOT.ML	Tue Oct 31 08:53:12 2000 +0100
@@ -1,4 +1,5 @@
 use "../settings.ML";
+use_thy "Typedef";
 use_thy "Overloading0";
 use_thy "Overloading2";
 use_thy "Axioms";
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Types/document/Axioms.tex
--- a/doc-src/TutorialI/Types/document/Axioms.tex	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Tue Oct 31 08:53:12 2000 +0100
@@ -59,7 +59,6 @@
 This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
 specialized to type \isa{bool}, as subgoals:
 \begin{isabelle}%
-OFCLASS{\isacharparenleft}bool{\isacharcomma}\ parord{\isacharunderscore}class{\isacharparenright}\isanewline
 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline
 \ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline
diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Types/types.tex
--- a/doc-src/TutorialI/Types/types.tex	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Types/types.tex	Tue Oct 31 08:53:12 2000 +0100
@@ -9,11 +9,13 @@
   ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason
   about them.
 \item Introducing your own types: how to introduce your own new types that
-  cannot be constructed with any of the basic methods ({\S}\ref{sec:typedef}).
+  cannot be constructed with any of the basic methods ({\S}\ref{sec:adv-typedef}).
 \item Type classes: how to specify and reason about axiomatic collections of
   types ({\S}\ref{sec:axclass}).
 \end{itemize}
 
+\input{Types/document/Typedef}
+
 \section{Axiomatic type classes}
 \label{sec:axclass}
 \index{axiomatic type class|(}
@@ -42,7 +44,7 @@
 
 \index{overloading|)}
 
-\input{Types/document/Axioms0}
+\input{Types/document/Axioms}
 
 \index{axiomatic type class|)}
 \index{*axclass|)}