*** empty log message ***

--- a/doc-src/TutorialI/Advanced/advanced.tex	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Advanced/advanced.tex	Wed Nov 08 14:38:04 2000 +0100
@@ -1,5 +1,4 @@
 \chapter{Advanced Simplification, Recursion and Induction}
-\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION, RECURSION ...}
 
 Although we have already learned a lot about simplification, recursion and
 induction, there are some advanced proof techniques that we have not covered

--- a/doc-src/TutorialI/Datatype/Fundata.thy	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Wed Nov 08 14:38:04 2000 +0100
@@ -1,17 +1,17 @@
 (*<*)
 theory Fundata = Main:
 (*>*)
-datatype ('a,'i)bigtree = Tip | Branch 'a "'i \<Rightarrow> ('a,'i)bigtree"
+datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
 
 text{*\noindent
 Parameter @{typ"'a"} is the type of values stored in
-the @{term"Branch"}es of the tree, whereas @{typ"'i"} is the index
+the @{term Br}anches of the tree, whereas @{typ"'i"} is the index
 type over which the tree branches. If @{typ"'i"} is instantiated to
 @{typ"bool"}, the result is a binary tree; if it is instantiated to
 @{typ"nat"}, we have an infinitely branching tree because each node
 has as many subtrees as there are natural numbers. How can we possibly
 write down such a tree? Using functional notation! For example, the term
-@{term[display]"Branch 0 (%i. Branch i (%n. Tip))"}
+@{term[display]"Br 0 (%i. Br i (%n. Tip))"}
 of type @{typ"(nat,nat)bigtree"} is the tree whose
 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
 has merely @{term"Tip"}s as further subtrees.
@@ -21,8 +21,8 @@
 
 consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
 primrec
-"map_bt f Tip          = Tip"
-"map_bt f (Branch a F) = Branch (f a) (\<lambda>i. map_bt f (F i))"
+"map_bt f Tip      = Tip"
+"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"
 
 text{*\noindent This is a valid \isacommand{primrec} definition because the
 recursive calls of @{term"map_bt"} involve only subtrees obtained from
@@ -37,19 +37,14 @@
 lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
 apply(induct_tac T, simp_all)
 done
-
-text{*\noindent
-%apply(induct_tac T);
-%pr(latex xsymbols symbols)
+(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
+apply(induct_tac T, rename_tac[2] F)(*>*)
+txt{*\noindent
 but it is worth taking a look at the proof state after the induction step
 to understand what the presence of the function type entails:
-\begin{isabelle}
-\ \isadigit{1}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
-\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline
-\ \ \ \ \ \ \ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
-\ \ \ \ \ \ \ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}{\isacharparenright}
-\end{isabelle}
+@{subgoals[display,indent=0]}
 *}
 (*<*)
+oops
 end
 (*>*)

--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Wed Nov 08 14:38:04 2000 +0100
@@ -1,18 +1,18 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Fundata}%
-\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Br\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 Parameter \isa{{\isacharprime}a} is the type of values stored in
-the \isa{Branch}es of the tree, whereas \isa{{\isacharprime}i} is the index
+the \isa{Br}anches of the tree, whereas \isa{{\isacharprime}i} is the index
 type over which the tree branches. If \isa{{\isacharprime}i} is instantiated to
 \isa{bool}, the result is a binary tree; if it is instantiated to
 \isa{nat}, we have an infinitely branching tree because each node
 has as many subtrees as there are natural numbers. How can we possibly
 write down such a tree? Using functional notation! For example, the term
 \begin{isabelle}%
-\ \ \ \ \ Branch\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
+\ \ \ \ \ Br\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
 \end{isabelle}
 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
@@ -22,8 +22,8 @@
 \end{isamarkuptext}%
 \isacommand{consts}\ map{\isacharunderscore}bt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline
-{\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline
-{\isachardoublequote}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+{\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline
+{\isachardoublequote}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Br\ a\ F{\isacharparenright}\ {\isacharequal}\ Br\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent This is a valid \isacommand{primrec} definition because the
 recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees obtained from
@@ -38,19 +38,16 @@
 \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
 \isacommand{done}%
-\begin{isamarkuptext}%
+\begin{isamarkuptxt}%
 \noindent
-%apply(induct_tac T);
-%pr(latex xsymbols symbols)
 but it is worth taking a look at the proof state after the induction step
 to understand what the presence of the function type entails:
-\begin{isabelle}
-\ \isadigit{1}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
-\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline
-\ \ \ \ \ \ \ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
-\ \ \ \ \ \ \ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}{\isacharparenright}
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ \ \ \ \ \ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Br\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Br\ a\ F{\isacharparenright}{\isacharparenright}%
 \end{isabelle}%
-\end{isamarkuptext}%
+\end{isamarkuptxt}%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/Inductive/AB.thy	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy	Wed Nov 08 14:38:04 2000 +0100
@@ -105,7 +105,7 @@
 @{thm[display]nat0_intermed_int_val[no_vars]}
 where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
 @{term abs} is the absolute value function, and @{term"#1::int"} is the
-integer 1 (see \S\ref{sec:int}).
+integer 1 (see \S\ref{sec:numbers}).
 
 First we show that the our specific function, the difference between the
 numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
@@ -120,7 +120,7 @@
        int(size[x\<in>take (i+1) w. \<not>P x]))
       -
       (int(size[x\<in>take i w.  P x]) -
-       int(size[x\<in>take i w. \<not>P x]))) <= #1";
+       int(size[x\<in>take i w. \<not>P x]))) \<le> #1";
 
 txt{*\noindent
 The lemma is a bit hard to read because of the coercion function

--- a/doc-src/TutorialI/Inductive/document/AB.tex	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Wed Nov 08 14:38:04 2000 +0100
@@ -101,7 +101,7 @@
 \end{isabelle}
 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
 \isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
-integer 1 (see \S\ref{sec:int}).
+integer 1 (see \S\ref{sec:numbers}).
 
 First we show that the our specific function, the difference between the
 numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
@@ -115,7 +115,7 @@
 \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
 \ \ \ \ \ \ {\isacharminus}\isanewline
 \ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
-\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
+\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 The lemma is a bit hard to read because of the coercion function

--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Nov 08 14:38:04 2000 +0100
@@ -51,23 +51,20 @@
 (*<*)oops;(*>*)
 lemma hd_rev: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
 (*<*)
-by(induct_tac xs, auto);
+apply(induct_tac xs);
 (*>*)
 
-text{*\noindent
+txt{*\noindent
 This time, induction leaves us with the following base case
-\begin{isabelle}
-\ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
-\end{isabelle}
+@{subgoals[display,indent=0,goals_limit=1]}
 which is trivial, and @{text"auto"} finishes the whole proof.
 
-If @{thm[source]hd_rev} is meant to be a simplification rule, you are
+If @{text hd_rev} is meant to be a simplification rule, you are
 done. But if you really need the @{text"\<Longrightarrow>"}-version of
-@{thm[source]hd_rev}, for example because you want to apply it as an
+@{text hd_rev}, for example because you want to apply it as an
 introduction rule, you need to derive it separately, by combining it with
 modus ponens:
-*};
-
+*}(*<*)by(auto);(*>*)
 lemmas hd_revI = hd_rev[THEN mp];
  
 text{*\noindent

--- a/doc-src/TutorialI/Misc/Itrev.thy	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Wed Nov 08 14:38:04 2000 +0100
@@ -61,9 +61,7 @@
 
 txt{*\noindent
 Unfortunately, this is not a complete success:
-\begin{isabelle}\makeatother
-~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
-\end{isabelle}
+@{subgoals[display,indent=0,margin=65]}
 Just as predicted above, the overall goal, and hence the induction
 hypothesis, is too weak to solve the induction step because of the fixed
 @{term"[]"}. The corresponding heuristic:

--- a/doc-src/TutorialI/Misc/case_exprs.thy	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/case_exprs.thy	Wed Nov 08 14:38:04 2000 +0100
@@ -58,10 +58,7 @@
 
 txt{*\noindent
 results in the proof state
-\begin{isabelle}
-~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
-~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
-\end{isabelle}
+@{subgoals[display,indent=0,margin=65]}
 which is solved automatically:
 *}
 

--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Nov 08 14:38:04 2000 +0100
@@ -53,11 +53,11 @@
 This means we should prove%
 \end{isamarkuptxt}%
 \isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}%
-\begin{isamarkuptext}%
+\begin{isamarkuptxt}%
 \noindent
 This time, induction leaves us with the following base case
-\begin{isabelle}
-\ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
 \end{isabelle}
 which is trivial, and \isa{auto} finishes the whole proof.
 
@@ -66,7 +66,7 @@
 \isa{hd{\isacharunderscore}rev}, for example because you want to apply it as an
 introduction rule, you need to derive it separately, by combining it with
 modus ponens:%
-\end{isamarkuptext}%
+\end{isamarkuptxt}%
 \isacommand{lemmas}\ hd{\isacharunderscore}revI\ {\isacharequal}\ hd{\isacharunderscore}rev{\isacharbrackleft}THEN\ mp{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent

--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Wed Nov 08 14:38:04 2000 +0100
@@ -60,8 +60,9 @@
 \begin{isamarkuptxt}%
 \noindent
 Unfortunately, this is not a complete success:
-\begin{isabelle}\makeatother
-~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
+\ \ \ \ \ \ \ itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
 \end{isabelle}
 Just as predicted above, the overall goal, and hence the induction
 hypothesis, is too weak to solve the induction step because of the fixed

--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Wed Nov 08 14:38:04 2000 +0100
@@ -67,9 +67,10 @@
 \begin{isamarkuptxt}%
 \noindent
 results in the proof state
-\begin{isabelle}
-~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
-~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
+\ \ \ \ \ \ \ xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs%
 \end{isabelle}
 which is solved automatically:%
 \end{isamarkuptxt}%

--- a/doc-src/TutorialI/Types/Axioms.thy	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Types/Axioms.thy	Wed Nov 08 14:38:04 2000 +0100
@@ -29,6 +29,12 @@
 @{text parord}. For example, this is what @{thm[source]refl} really looks like:
 @{thm[show_types]refl}.
 
+We have not made @{thm[source]less_le} a global definition because it would
+fix once and for all that @{text"<<"} is defined in terms of @{text"<<="}.
+There are however situations where it is the other way around, which such a
+definition would complicate. The slight drawback of the above class is that
+we need to define both @{text"<<="} and @{text"<<"} for each instance.
+
 We can now prove simple theorems in this abstract setting, for example
 that @{text"<<"} is not symmetric:
 *}

--- a/doc-src/TutorialI/Types/Typedef.thy	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Types/Typedef.thy	Wed Nov 08 14:38:04 2000 +0100
@@ -11,7 +11,7 @@
 then read on.
 \begin{warn}
   Types in HOL must be non-empty; otherwise the quantifier rules would be
-  unsound, because $\exists x. x=x$ is a theorem.
+  unsound, because $\exists x.\ x=x$ is a theorem.
 \end{warn}
 *}
 
@@ -24,8 +24,8 @@
 typedecl my_new_type
 
 text{*\noindent\indexbold{*typedecl}%
-This does not define the type at all but merely introduces its name, @{typ
-my_new_type}. Thus we know nothing about this type, except that it is
+This does not define @{typ my_new_type} at all but merely introduces its
+name. Thus we know nothing about this type, except that it is
 non-empty. Such declarations without definitions are
 useful only if that type can be viewed as a parameter of a theory and we do
 not intend to impose any restrictions on it. A typical example is given in
@@ -43,7 +43,7 @@
 *}
 
 axioms
-just_one: "\<exists>! x::my_new_type. True"
+just_one: "\<exists>x::my_new_type. \<forall>y. x = y"
 
 text{*\noindent
 However, we strongly discourage this approach, except at explorative stages

--- a/doc-src/TutorialI/Types/document/Axioms.tex	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Wed Nov 08 14:38:04 2000 +0100
@@ -32,6 +32,12 @@
 \isa{parord}. For example, this is what \isa{refl} really looks like:
 \isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
 
+We have not made \isa{less{\isacharunderscore}le} a global definition because it would
+fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}}.
+There are however situations where it is the other way around, which such a
+definition would complicate. The slight drawback of the above class is that
+we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance.
+
 We can now prove simple theorems in this abstract setting, for example
 that \isa{{\isacharless}{\isacharless}} is not symmetric:%
 \end{isamarkuptext}%

--- a/doc-src/TutorialI/Types/document/Typedef.tex	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex	Wed Nov 08 14:38:04 2000 +0100
@@ -15,7 +15,7 @@
 then read on.
 \begin{warn}
   Types in HOL must be non-empty; otherwise the quantifier rules would be
-  unsound, because $\exists x. x=x$ is a theorem.
+  unsound, because $\exists x.\ x=x$ is a theorem.
 \end{warn}%
 \end{isamarkuptext}%
 %
@@ -30,7 +30,8 @@
 \isacommand{typedecl}\ my{\isacharunderscore}new{\isacharunderscore}type%
 \begin{isamarkuptext}%
 \noindent\indexbold{*typedecl}%
-This does not define the type at all but merely introduces its name, \isa{my{\isacharunderscore}new{\isacharunderscore}type}. Thus we know nothing about this type, except that it is
+This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its
+name. Thus we know nothing about this type, except that it is
 non-empty. Such declarations without definitions are
 useful only if that type can be viewed as a parameter of a theory and we do
 not intend to impose any restrictions on it. A typical example is given in
@@ -47,7 +48,7 @@
 axioms. Example:%
 \end{isamarkuptext}%
 \isacommand{axioms}\isanewline
-just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}{\isacharbang}\ x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ True{\isachardoublequote}%
+just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ {\isasymforall}y{\isachardot}\ x\ {\isacharequal}\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 However, we strongly discourage this approach, except at explorative stages

--- a/doc-src/TutorialI/Types/types.tex	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Types/types.tex	Wed Nov 08 14:38:04 2000 +0100
@@ -22,6 +22,7 @@
 \subsection{Pairs}
 \label{sec:products}
 % Check refs to this section to see what is expected of it.
+% Mention type unit
 
 \subsection{Records}
 \label{sec:records}