
diff -r 135317cd34d6 -r 1992553cccfe doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Fri Oct 31 10:39:04 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Mon Nov 03 14:15:25 2008 +0100
@@ -87,11 +87,11 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline%
-\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline%
-\verb|dequeue (Queue xs []) =|\newline%
-\verb|  (if nulla xs then (Nothing, Queue [] [])|\newline%
-\verb|    else dequeue (Queue [] (rev xs)));|%
+\hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\
+\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\
+\hspace*{0pt}dequeue (Queue xs []) =\\
+\hspace*{0pt} ~(if nulla xs then (Nothing, Queue [] [])\\
+\hspace*{0pt} ~~~else dequeue (Queue [] (rev xs)));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -273,46 +273,46 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|module Example where {|\newline%
-\newline%
-\newline%
-\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
-\newline%
-\verb|class Semigroup a where {|\newline%
-\verb|  mult :: a -> a -> a;|\newline%
-\verb|};|\newline%
-\newline%
-\verb|class (Semigroup a) => Monoid a where {|\newline%
-\verb|  neutral :: a;|\newline%
-\verb|};|\newline%
-\newline%
-\verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
-\verb|pow Zero_nat a = neutral;|\newline%
-\verb|pow (Suc n) a = mult a (pow n a);|\newline%
-\newline%
-\verb|plus_nat :: Nat -> Nat -> Nat;|\newline%
-\verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline%
-\verb|plus_nat Zero_nat n = n;|\newline%
-\newline%
-\verb|neutral_nat :: Nat;|\newline%
-\verb|neutral_nat = Suc Zero_nat;|\newline%
-\newline%
-\verb|mult_nat :: Nat -> Nat -> Nat;|\newline%
-\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
-\verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
-\newline%
-\verb|instance Semigroup Nat where {|\newline%
-\verb|  mult = mult_nat;|\newline%
-\verb|};|\newline%
-\newline%
-\verb|instance Monoid Nat where {|\newline%
-\verb|  neutral = neutral_nat;|\newline%
-\verb|};|\newline%
-\newline%
-\verb|bexp :: Nat -> Nat;|\newline%
-\verb|bexp n = pow n (Suc (Suc Zero_nat));|\newline%
-\newline%
-\verb|}|%
+\hspace*{0pt}module Example where {\char123}\\
+\hspace*{0pt}\\
+\hspace*{0pt}\\
+\hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}class Semigroup a where {\char123}\\
+\hspace*{0pt} ~mult ::~a -> a -> a;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
+\hspace*{0pt} ~neutral ::~a;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}pow ::~forall a. (Monoid a) => Nat -> a -> a;\\
+\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
+\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
+\hspace*{0pt}\\
+\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
+\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
+\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
+\hspace*{0pt}\\
+\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
+\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
+\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
+\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Semigroup Nat where {\char123}\\
+\hspace*{0pt} ~mult = mult{\char95}nat;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Monoid Nat where {\char123}\\
+\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}bexp ::~Nat -> Nat;\\
+\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
+\hspace*{0pt}\\
+\hspace*{0pt}{\char125}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -338,38 +338,38 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|structure Example = |\newline%
-\verb|struct|\newline%
-\newline%
-\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
-\newline%
-\verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline%
-\verb|fun mult (A_:'a semigroup) = #mult A_;|\newline%
-\newline%
-\verb|type 'a monoid = {Program__semigroup_monoid : 'a semigroup, neutral : 'a};|\newline%
-\verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline%
-\verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline%
-\newline%
-\verb|fun pow A_ Zero_nat a = neutral A_|\newline%
-\verb|  |\verb,|,\verb| pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a);|\newline%
-\newline%
-\verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline%
-\verb|  |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
-\newline%
-\verb|val neutral_nat : nat = Suc Zero_nat;|\newline%
-\newline%
-\verb|fun mult_nat Zero_nat n = Zero_nat|\newline%
-\verb|  |\verb,|,\verb| mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
-\newline%
-\verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline%
-\newline%
-\verb|val monoid_nat =|\newline%
-\verb|  {Program__semigroup_monoid = semigroup_nat, neutral = neutral_nat} :|\newline%
-\verb|  nat monoid;|\newline%
-\newline%
-\verb|fun bexp n = pow monoid_nat n (Suc (Suc Zero_nat));|\newline%
-\newline%
-\verb|end; (*struct Example*)|%
+\hspace*{0pt}structure Example = \\
+\hspace*{0pt}struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
+\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup, neutral :~'a{\char125};\\
+\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\
+\hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
+\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
+\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
+\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
+\hspace*{0pt}\\
+\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val monoid{\char95}nat =\\
+\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat, neutral = neutral{\char95}nat{\char125}~:\\
+\hspace*{0pt} ~nat monoid;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
+\hspace*{0pt}\\
+\hspace*{0pt}end; (*struct Example*)%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -659,23 +659,23 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|structure Example = |\newline%
-\verb|struct|\newline%
-\newline%
-\verb|datatype nat = Dig1 of nat |\verb,|,\verb| Dig0 of nat |\verb,|,\verb| One_nat |\verb,|,\verb| Zero_nat;|\newline%
-\newline%
-\verb|fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat)|\newline%
-\verb|  |\verb,|,\verb| plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n)|\newline%
-\verb|  |\verb,|,\verb| plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n)|\newline%
-\verb|  |\verb,|,\verb| plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n)|\newline%
-\verb|  |\verb,|,\verb| plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat)|\newline%
-\verb|  |\verb,|,\verb| plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat)|\newline%
-\verb|  |\verb,|,\verb| plus_nat (Dig0 m) One_nat = Dig1 m|\newline%
-\verb|  |\verb,|,\verb| plus_nat One_nat (Dig0 n) = Dig1 n|\newline%
-\verb|  |\verb,|,\verb| plus_nat m Zero_nat = m|\newline%
-\verb|  |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
-\newline%
-\verb|end; (*struct Example*)|%
+\hspace*{0pt}structure Example = \\
+\hspace*{0pt}struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype nat = Dig1 of nat | Dig0 of nat | One{\char95}nat | Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun plus{\char95}nat (Dig1 m) (Dig1 n) = Dig0 (plus{\char95}nat (plus{\char95}nat m n) One{\char95}nat)\\
+\hspace*{0pt} ~| plus{\char95}nat (Dig1 m) (Dig0 n) = Dig1 (plus{\char95}nat m n)\\
+\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig1 n) = Dig1 (plus{\char95}nat m n)\\
+\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig0 n) = Dig0 (plus{\char95}nat m n)\\
+\hspace*{0pt} ~| plus{\char95}nat (Dig1 m) One{\char95}nat = Dig0 (plus{\char95}nat m One{\char95}nat)\\
+\hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig1 n) = Dig0 (plus{\char95}nat n One{\char95}nat)\\
+\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) One{\char95}nat = Dig1 m\\
+\hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig0 n) = Dig1 n\\
+\hspace*{0pt} ~| plus{\char95}nat m Zero{\char95}nat = m\\
+\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
+\hspace*{0pt}\\
+\hspace*{0pt}end; (*struct Example*)%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -776,25 +776,25 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|structure Example = |\newline%
-\verb|struct|\newline%
-\newline%
-\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
-\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
-\newline%
-\verb|fun eqop A_ a b = eq A_ a b;|\newline%
-\newline%
-\verb|fun member A_ x [] = false|\newline%
-\verb|  |\verb,|,\verb| member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys;|\newline%
-\newline%
-\verb|fun collect_duplicates A_ xs ys [] = xs|\newline%
-\verb|  |\verb,|,\verb| collect_duplicates A_ xs ys (z :: zs) =|\newline%
-\verb|    (if member A_ z xs|\newline%
-\verb|      then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
-\verb|             else collect_duplicates A_ xs (z :: ys) zs)|\newline%
-\verb|      else collect_duplicates A_ (z :: xs) (z :: ys) zs);|\newline%
-\newline%
-\verb|end; (*struct Example*)|%
+\hspace*{0pt}structure Example = \\
+\hspace*{0pt}struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
+\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun member A{\char95}~x [] = false\\
+\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqop A{\char95}~x y orelse member A{\char95}~x ys;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
+\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
+\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
+\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
+\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
+\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
+\hspace*{0pt}\\
+\hspace*{0pt}end; (*struct Example*)%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -912,34 +912,34 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|structure Example = |\newline%
-\verb|struct|\newline%
-\newline%
-\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
-\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
-\newline%
-\verb|type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};|\newline%
-\verb|fun less_eq (A_:'a ord) = #less_eq A_;|\newline%
-\verb|fun less (A_:'a ord) = #less A_;|\newline%
-\newline%
-\verb|fun eqop A_ a b = eq A_ a b;|\newline%
-\newline%
-\verb|type 'a preorder = {Orderings__ord_preorder : 'a ord};|\newline%
-\verb|fun ord_preorder (A_:'a preorder) = #Orderings__ord_preorder A_;|\newline%
-\newline%
-\verb|type 'a order = {Orderings__preorder_order : 'a preorder};|\newline%
-\verb|fun preorder_order (A_:'a order) = #Orderings__preorder_order A_;|\newline%
-\newline%
-\verb|fun less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline%
-\verb|  less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline%
-\verb|    eqop A1_ x1 x2 andalso|\newline%
-\verb|      less_eq ((ord_preorder o preorder_order) B_) y1 y2|\newline%
-\verb|  |\verb,|,\verb| less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline%
-\verb|    less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline%
-\verb|      eqop A1_ x1 x2 andalso|\newline%
-\verb|        less_eq ((ord_preorder o preorder_order) B_) y1 y2;|\newline%
-\newline%
-\verb|end; (*struct Example*)|%
+\hspace*{0pt}structure Example = \\
+\hspace*{0pt}struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
+\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool, less :~'a -> 'a -> bool{\char125};\\
+\hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\
+\hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a preorder = {\char123}Orderings{\char95}{\char95}ord{\char95}preorder :~'a ord{\char125};\\
+\hspace*{0pt}fun ord{\char95}preorder (A{\char95}:'a preorder) = {\char35}Orderings{\char95}{\char95}ord{\char95}preorder A{\char95};\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\
+\hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\
+\hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
+\hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\
+\hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\
+\hspace*{0pt} ~| less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\
+\hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
+\hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\
+\hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\
+\hspace*{0pt}\\
+\hspace*{0pt}end; (*struct Example*)%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1033,29 +1033,29 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|structure Example = |\newline%
-\verb|struct|\newline%
-\newline%
-\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
-\newline%
-\verb|fun null [] = true|\newline%
-\verb|  |\verb,|,\verb| null (x :: xs) = false;|\newline%
-\newline%
-\verb|fun eq_nat (Suc a) Zero_nat = false|\newline%
-\verb|  |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline%
-\verb|  |\verb,|,\verb| eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'|\newline%
-\verb|  |\verb,|,\verb| eq_nat Zero_nat Zero_nat = true;|\newline%
-\newline%
-\verb|datatype monotype = Mono of nat * monotype list;|\newline%
-\newline%
-\verb|fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys|\newline%
-\verb|  |\verb,|,\verb| list_all2 p xs [] = null xs|\newline%
-\verb|  |\verb,|,\verb| list_all2 p [] ys = null ys;|\newline%
-\newline%
-\verb|fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =|\newline%
-\verb|  eq_nat tyco1 tyco2 andalso list_all2 eq_monotype typargs1 typargs2;|\newline%
-\newline%
-\verb|end; (*struct Example*)|%
+\hspace*{0pt}structure Example = \\
+\hspace*{0pt}struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun null [] = true\\
+\hspace*{0pt} ~| null (x ::~xs) = false;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun eq{\char95}nat (Suc a) Zero{\char95}nat = false\\
+\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc a) = false\\
+\hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\
+\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\
+\hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\
+\hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =\\
+\hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\
+\hspace*{0pt}\\
+\hspace*{0pt}end; (*struct Example*)%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1108,12 +1108,12 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|strict_dequeue :: forall a. Queue a -> (a, Queue a);|\newline%
-\verb|strict_dequeue (Queue xs (y : ys)) = (y, Queue xs ys);|\newline%
-\verb|strict_dequeue (Queue xs []) =|\newline%
-\verb|  let {|\newline%
-\verb|    (y : ys) = rev xs;|\newline%
-\verb|  } in (y, Queue [] ys);|%
+\hspace*{0pt}strict{\char95}dequeue ::~forall a. Queue a -> (a, Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y, Queue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue (Queue xs []) =\\
+\hspace*{0pt} ~let {\char123}\\
+\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
+\hspace*{0pt} ~{\char125}~in (y, Queue [] ys);%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1204,13 +1204,13 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|empty_queue :: forall a. a;|\newline%
-\verb|empty_queue = error "empty_queue";|\newline%
-\newline%
-\verb|strict_dequeue' :: forall a. Queue a -> (a, Queue a);|\newline%
-\verb|strict_dequeue' (Queue xs []) =|\newline%
-\verb|  (if nulla xs then empty_queue else strict_dequeue' (Queue [] (rev xs)));|\newline%
-\verb|strict_dequeue' (Queue xs (y : ys)) = (y, Queue xs ys);|%
+\hspace*{0pt}empty{\char95}queue ::~forall a. a;\\
+\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
+\hspace*{0pt}\\
+\hspace*{0pt}strict{\char95}dequeue' ::~forall a. Queue a -> (a, Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue' (Queue xs []) =\\
+\hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue' (Queue [] (rev xs)));\\
+\hspace*{0pt}strict{\char95}dequeue' (Queue xs (y :~ys)) = (y, Queue xs ys);%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %




