# HG changeset patch
# User nipkow
# Date 1007139313 -3600
# Node ID 60bf75e157e44632fcbd7e5f1b2ef371217fd723
# Parent  ef43a3d6e962460e175ecd56b005de394df9dd87
*** empty log message ***

diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/Advanced/Partial.thy
--- a/doc-src/TutorialI/Advanced/Partial.thy	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Fri Nov 30 17:55:13 2001 +0100
@@ -62,9 +62,9 @@
 *}
 
 consts divi :: "nat \<times> nat \<Rightarrow> nat"
-recdef (permissive) divi "measure(\<lambda>(m,n). m)"
-  "divi(m,n) = (if n = 0 then arbitrary else
-                if m < n then 0 else divi(m-n,n)+1)"  (* FIXME hide permissive!? *)
+recdef divi "measure(\<lambda>(m,n). m)"
+  "divi(m,0) = arbitrary"
+  "divi(m,n) = (if m < n then 0 else divi(m-n,n)+1)"
 
 text{*\noindent Of course we could also have defined
 @{term"divi(m,0)"} to be some specific number, for example 0. The
@@ -75,12 +75,12 @@
 As a more substantial example we consider the problem of searching a graph.
 For simplicity our graph is given by a function @{term f} of
 type @{typ"'a \<Rightarrow> 'a"} which
-maps each node to its successor; the graph is really a tree.
+maps each node to its successor; the graph has out-degree 1.
 The task is to find the end of a chain, modelled by a node pointing to
 itself. Here is a first attempt:
 @{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"}
-This may be viewed as a fixed point finder or as one half of the well known
-\emph{Union-Find} algorithm.
+This may be viewed as a fixed point finder or as the second half of the well
+known \emph{Union-Find} algorithm.
 The snag is that it may not terminate if @{term f} has non-trivial cycles.
 Phrased differently, the relation
 *}
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/Advanced/document/Partial.tex
--- a/doc-src/TutorialI/Advanced/document/Partial.tex	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Fri Nov 30 17:55:13 2001 +0100
@@ -74,9 +74,9 @@
 \isamarkuptrue%
 \isacommand{consts}\ divi\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{recdef}\ {\isacharparenleft}\isakeyword{permissive}{\isacharparenright}\ divi\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ arbitrary\ else\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ if\ m\ {\isacharless}\ n\ then\ {\isadigit{0}}\ else\ divi{\isacharparenleft}m{\isacharminus}n{\isacharcomma}n{\isacharparenright}{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isacommand{recdef}\ divi\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ arbitrary{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ {\isadigit{0}}\ else\ divi{\isacharparenleft}m{\isacharminus}n{\isacharcomma}n{\isacharparenright}{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Of course we could also have defined
@@ -88,14 +88,14 @@
 As a more substantial example we consider the problem of searching a graph.
 For simplicity our graph is given by a function \isa{f} of
 type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which
-maps each node to its successor; the graph is really a tree.
+maps each node to its successor; the graph has out-degree 1.
 The task is to find the end of a chain, modelled by a node pointing to
 itself. Here is a first attempt:
 \begin{isabelle}%
 \ \ \ \ \ find\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find\ {\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}%
 \end{isabelle}
-This may be viewed as a fixed point finder or as one half of the well known
-\emph{Union-Find} algorithm.
+This may be viewed as a fixed point finder or as the second half of the well
+known \emph{Union-Find} algorithm.
 The snag is that it may not terminate if \isa{f} has non-trivial cycles.
 Phrased differently, the relation%
 \end{isamarkuptext}%
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Nov 30 17:55:13 2001 +0100
@@ -455,17 +455,16 @@
 done
 *)
 (*>*)
-text{*
-Let us close this section with a few words about the executability of our model checkers.
-It is clear that if all sets are finite, they can be represented as lists and the usual
-set operations are easily implemented. Only @{term lfp} requires a little thought.
-Fortunately, the
-Library\footnote{See theory \isa{While_Combinator}.}~\cite{isabelle-HOL-lib}
-provides a theorem stating that 
-in the case of finite sets and a monotone function~@{term F},
-the value of \mbox{@{term"lfp F"}} can be computed by iterated application of @{term F} to~@{term"{}"} until
-a fixed point is reached. It is actually possible to generate executable functional programs
+
+text{* Let us close this section with a few words about the executability of
+our model checkers.  It is clear that if all sets are finite, they can be
+represented as lists and the usual set operations are easily
+implemented. Only @{term lfp} requires a little thought.  Fortunately, theory
+@{text While_Combinator} in the Library~\cite{isabelle-HOL-lib} provides a
+theorem stating that in the case of finite sets and a monotone
+function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by
+iterated application of @{term F} to~@{term"{}"} until a fixed point is
+reached. It is actually possible to generate executable functional programs
 from HOL definitions, but that is beyond the scope of the tutorial.%
-\index{CTL|)}
-*}
+\index{CTL|)} *}
 (*<*)end(*>*)
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/CTL/document/CTL.tex
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Fri Nov 30 17:55:13 2001 +0100
@@ -465,15 +465,15 @@
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
-Let us close this section with a few words about the executability of our model checkers.
-It is clear that if all sets are finite, they can be represented as lists and the usual
-set operations are easily implemented. Only \isa{lfp} requires a little thought.
-Fortunately, the
-Library\footnote{See theory \isa{While_Combinator}.}~\cite{isabelle-HOL-lib}
-provides a theorem stating that 
-in the case of finite sets and a monotone function~\isa{F},
-the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
-a fixed point is reached. It is actually possible to generate executable functional programs
+Let us close this section with a few words about the executability of
+our model checkers.  It is clear that if all sets are finite, they can be
+represented as lists and the usual set operations are easily
+implemented. Only \isa{lfp} requires a little thought.  Fortunately, theory
+\isa{While{\isacharunderscore}Combinator} in the Library~\cite{isabelle-HOL-lib} provides a
+theorem stating that in the case of finite sets and a monotone
+function~\isa{F}, the value of \mbox{\isa{lfp\ F}} can be computed by
+iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until a fixed point is
+reached. It is actually possible to generate executable functional programs
 from HOL definitions, but that is beyond the scope of the tutorial.%
 \index{CTL|)}%
 \end{isamarkuptext}%
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/Datatype/ABexpr.thy
--- a/doc-src/TutorialI/Datatype/ABexpr.thy	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Fri Nov 30 17:55:13 2001 +0100
@@ -123,9 +123,50 @@
   Prove that @{text"norma"}
   preserves the value of an expression and that the result of @{text"norma"}
   is really normal, i.e.\ no more @{term"And"}s and @{term"Neg"}s occur in
-  it.  ({\em Hint:} proceed as in \S\ref{sec:boolex}).
+  it.  ({\em Hint:} proceed as in \S\ref{sec:boolex} and read the discussion
+  of type annotations following lemma @{text subst_id} below).
 \end{exercise}
 *}
-(*<*) 
+(*<*)
+consts norma :: "'a aexp \<Rightarrow> 'a aexp"
+       normb :: "'a bexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp"
+
+primrec
+"norma (IF b t e)   = (normb b (norma t) (norma e))"
+"norma (Sum a1 a2)  = Sum (norma a1) (norma a2)" 
+"norma (Diff a1 a2) = Diff (norma a1) (norma a2)"
+"norma (Var v)      = Var v"
+"norma (Num n)      = Num n"
+            
+"normb (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e"
+"normb (And b1 b2)  t e = normb b1 (normb b2 t e) e"
+"normb (Neg b)      t e = normb b e t"
+
+lemma " evala (norma a) env = evala a env 
+      \<and> (\<forall> t e. evala (normb b t e) env = evala (IF b t e) env)"
+apply (induct_tac a and b)
+apply (simp_all)
+done
+
+consts normala :: "'a aexp \<Rightarrow> bool"
+       normalb :: "'b bexp \<Rightarrow> bool"
+
+primrec
+"normala (IF b t e)   = (normalb b \<and> normala t \<and> normala e)"
+"normala (Sum a1 a2)  = (normala a1 \<and> normala a2)"
+"normala (Diff a1 a2) = (normala a1 \<and> normala a2)"
+"normala (Var v)      = True"
+"normala (Num n)      = True"
+
+"normalb (Less a1 a2) = (normala a1 \<and> normala a2)"
+"normalb (And b1 b2)  = False"
+"normalb (Neg b)      = False"
+
+lemma "normala (norma (a::'a aexp)) \<and>
+       (\<forall> (t::'a aexp) e. (normala t \<and> normala e) \<longrightarrow> normala (normb b t e))"
+apply (induct_tac a and b)
+apply (auto)
+done
+
 end
 (*>*)
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/Datatype/Nested.thy
--- a/doc-src/TutorialI/Datatype/Nested.thy	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Fri Nov 30 17:55:13 2001 +0100
@@ -66,8 +66,8 @@
 strengthened and proved as follows:
 *}
 
-lemma "subst  Var t  = (t ::('v,'f)term)  \<and>
-        substs Var ts = (ts::('v,'f)term list)";
+lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst  Var t  = (t ::('v,'f)term)  \<and>
+                  substs Var ts = (ts::('v,'f)term list)";
 apply(induct_tac t and ts, simp_all);
 done
 
@@ -102,6 +102,34 @@
 insists on the conjunctive format. Fortunately, we can easily \emph{prove}
 that the suggested equation holds:
 *}
+(*<*)
+(* Exercise 1: *)
+lemma "subst  ((subst f) \<circ> g) t  = subst  f (subst g t) \<and>
+       substs ((subst f) \<circ> g) ts = substs f (substs g ts)"
+apply (induct_tac t and ts)
+apply (simp_all)
+done
+
+(* Exercise 2: *)
+
+consts trev :: "('v,'f) term \<Rightarrow> ('v,'f) term"
+       trevs:: "('v,'f) term list \<Rightarrow> ('v,'f) term list"
+primrec
+"trev (Var v)    = Var v"
+"trev (App f ts) = App f (trevs ts)"
+
+"trevs [] = []"
+"trevs (t#ts) = (trevs ts) @ [(trev t)]" 
+
+lemma [simp]: "\<forall> ys. trevs (xs @ ys) = (trevs ys) @ (trevs xs)" 
+apply (induct_tac xs, auto)
+done
+
+lemma "trev (trev t) = (t::('v,'f)term) \<and> 
+       trevs (trevs ts) = (ts::('v,'f)term list)"
+apply (induct_tac t and ts, simp_all)
+done
+(*>*)
 
 lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
 apply(induct_tac ts, simp_all)
@@ -130,6 +158,4 @@
 constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
 expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}.
 *}
-(*<*)
-end
-(*>*)
+(*<*)end(*>*)
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/Datatype/document/ABexpr.tex
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Fri Nov 30 17:55:13 2001 +0100
@@ -130,11 +130,24 @@
   Prove that \isa{norma}
   preserves the value of an expression and that the result of \isa{norma}
   is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in
-  it.  ({\em Hint:} proceed as in \S\ref{sec:boolex}).
+  it.  ({\em Hint:} proceed as in \S\ref{sec:boolex} and read the discussion
+  of type annotations following lemma \isa{subst{\isacharunderscore}id} below).
 \end{exercise}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/Datatype/document/Nested.tex
--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Fri Nov 30 17:55:13 2001 +0100
@@ -70,8 +70,8 @@
 strengthened and proved as follows:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
-\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ subst{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
 \isamarkupfalse%
@@ -114,6 +114,19 @@
 that the suggested equation holds:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/Types/Overloading2.thy
--- a/doc-src/TutorialI/Types/Overloading2.thy	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy	Fri Nov 30 17:55:13 2001 +0100
@@ -19,8 +19,8 @@
 
 \begin{warn}
 A type constructor can be instantiated in only one way to
-a given type class.  For example, our two instantiations of \isa{list} must
-reside in separate theories with disjoint scopes.\REMARK{Tobias, please check}
+a given type class.  For example, our two instantiations of @{text list} must
+reside in separate theories with disjoint scopes.
 \end{warn}
 *}
 
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/Types/Typedefs.thy
--- a/doc-src/TutorialI/Types/Typedefs.thy	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Types/Typedefs.thy	Fri Nov 30 17:55:13 2001 +0100
@@ -61,13 +61,9 @@
 Now we come to the most general means of safely introducing a new type, the
 \textbf{type definition}. All other means, for example
 \isacommand{datatype}, are based on it. The principle is extremely simple:
-any non-empty subset of an existing type can be turned into a new type.  Thus
-a type definition is merely a notational device: you introduce a new name for
-a subset of an existing type. This does not add any logical power to HOL,
-because you could base all your work directly on the subset of the existing
-type. However, the resulting theories could easily become indigestible
-because instead of implicit types you would have explicit sets in your
-formulae.
+any non-empty subset of an existing type can be turned into a new type.
+More precisely, the new type is specified to be isomorphic to some
+non-empty subset of an existing type.
 
 Let us work a simple example, the definition of a three-element type.
 It is easily represented by the first three natural numbers:
@@ -87,9 +83,9 @@
 
 text{*
 This type definition introduces the new type @{typ three} and asserts
-that it is a copy of the set @{term"{0,1,2}"}. This assertion
+that it is a copy of the set @{term"{0::nat,1,2}"}. This assertion
 is expressed via a bijection between the \emph{type} @{typ three} and the
-\emph{set} @{term"{0,1,2}"}. To this end, the command declares the following
+\emph{set} @{term"{0::nat,1,2}"}. To this end, the command declares the following
 constants behind the scenes:
 \begin{center}
 \begin{tabular}{rcl}
@@ -131,7 +127,7 @@
 %
 From this example it should be clear what \isacommand{typedef} does
 in general given a name (here @{text three}) and a set
-(here @{term"{n. n\<le>2}"}).
+(here @{term"{n::nat. n\<le>2}"}).
 
 Our next step is to define the basic functions expected on the new type.
 Although this depends on the type at hand, the following strategy works well:
@@ -246,7 +242,7 @@
 above lengthy definition can be collapsed into one line:
 *}
 
-datatype three' = A | B | C
+datatype better_three = A | B | C
 
 text{*\noindent
 In fact, the \isacommand{datatype} command performs internally more or less
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/Types/document/Overloading2.tex
--- a/doc-src/TutorialI/Types/document/Overloading2.tex	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Fri Nov 30 17:55:13 2001 +0100
@@ -26,7 +26,7 @@
 \begin{warn}
 A type constructor can be instantiated in only one way to
 a given type class.  For example, our two instantiations of \isa{list} must
-reside in separate theories with disjoint scopes.\REMARK{Tobias, please check}
+reside in separate theories with disjoint scopes.
 \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r ef43a3d6e962 -r 60bf75e157e4 doc-src/TutorialI/Types/document/Typedefs.tex
--- a/doc-src/TutorialI/Types/document/Typedefs.tex	Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex	Fri Nov 30 17:55:13 2001 +0100
@@ -78,13 +78,9 @@
 Now we come to the most general means of safely introducing a new type, the
 \textbf{type definition}. All other means, for example
 \isacommand{datatype}, are based on it. The principle is extremely simple:
-any non-empty subset of an existing type can be turned into a new type.  Thus
-a type definition is merely a notational device: you introduce a new name for
-a subset of an existing type. This does not add any logical power to HOL,
-because you could base all your work directly on the subset of the existing
-type. However, the resulting theories could easily become indigestible
-because instead of implicit types you would have explicit sets in your
-formulae.
+any non-empty subset of an existing type can be turned into a new type.
+More precisely, the new type is specified to be isomorphic to some
+non-empty subset of an existing type.
 
 Let us work a simple example, the definition of a three-element type.
 It is easily represented by the first three natural numbers:%
@@ -108,9 +104,9 @@
 %
 \begin{isamarkuptext}%
 This type definition introduces the new type \isa{three} and asserts
-that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharbraceright}}. This assertion
+that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. This assertion
 is expressed via a bijection between the \emph{type} \isa{three} and the
-\emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharbraceright}}. To this end, the command declares the following
+\emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. To this end, the command declares the following
 constants behind the scenes:
 \begin{center}
 \begin{tabular}{rcl}
@@ -151,7 +147,7 @@
 %
 From this example it should be clear what \isacommand{typedef} does
 in general given a name (here \isa{three}) and a set
-(here \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharbraceright}}).
+(here \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}).
 
 Our next step is to define the basic functions expected on the new type.
 Although this depends on the type at hand, the following strategy works well:
@@ -281,7 +277,7 @@
 above lengthy definition can be collapsed into one line:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{datatype}\ three{\isacharprime}\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isamarkupfalse%
+\isacommand{datatype}\ better{\isacharunderscore}three\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent