# HG changeset patch
# User haftmann
# Date 1225718125 -3600
# Node ID 1992553cccfed69abc652da2677feb63633c5caf
# Parent  135317cd34d650c5cba4021bda65d0c446502cde
improved verbatim mechanism

diff -r 135317cd34d6 -r 1992553cccfe doc-src/IsarAdvanced/Classes/IsaMakefile
--- a/doc-src/IsarAdvanced/Classes/IsaMakefile	Fri Oct 31 10:39:04 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/IsaMakefile	Mon Nov 03 14:15:25 2008 +0100
@@ -23,7 +23,7 @@
 
 Thy: $(THY)
 
-$(THY): Thy/ROOT.ML Thy/Classes.thy
+$(THY): Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy
 	@$(USEDIR) HOL Thy
 
 
diff -r 135317cd34d6 -r 1992553cccfe doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 31 10:39:04 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Mon Nov 03 14:15:25 2008 +0100
@@ -1116,69 +1116,69 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|module Example where {|\newline%
-\newline%
-\newline%
-\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
-\newline%
-\verb|nat_aux :: Integer -> Nat -> Nat;|\newline%
-\verb|nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));|\newline%
-\newline%
-\verb|nat :: Integer -> Nat;|\newline%
-\verb|nat i = nat_aux i Zero_nat;|\newline%
-\newline%
-\verb|class Semigroup a where {|\newline%
-\verb|  mult :: a -> a -> a;|\newline%
-\verb|};|\newline%
-\newline%
-\verb|class (Semigroup a) => Monoidl a where {|\newline%
-\verb|  neutral :: a;|\newline%
-\verb|};|\newline%
-\newline%
-\verb|class (Monoidl a) => Monoid a where {|\newline%
-\verb|};|\newline%
-\newline%
-\verb|class (Monoid a) => Group a where {|\newline%
-\verb|  inverse :: a -> a;|\newline%
-\verb|};|\newline%
-\newline%
-\verb|inverse_int :: Integer -> Integer;|\newline%
-\verb|inverse_int i = negate i;|\newline%
-\newline%
-\verb|neutral_int :: Integer;|\newline%
-\verb|neutral_int = 0;|\newline%
-\newline%
-\verb|mult_int :: Integer -> Integer -> Integer;|\newline%
-\verb|mult_int i j = i + j;|\newline%
-\newline%
-\verb|instance Semigroup Integer where {|\newline%
-\verb|  mult = mult_int;|\newline%
-\verb|};|\newline%
-\newline%
-\verb|instance Monoidl Integer where {|\newline%
-\verb|  neutral = neutral_int;|\newline%
-\verb|};|\newline%
-\newline%
-\verb|instance Monoid Integer where {|\newline%
-\verb|};|\newline%
-\newline%
-\verb|instance Group Integer where {|\newline%
-\verb|  inverse = inverse_int;|\newline%
-\verb|};|\newline%
-\newline%
-\verb|pow_nat :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
-\verb|pow_nat Zero_nat x = neutral;|\newline%
-\verb|pow_nat (Suc n) x = mult x (pow_nat n x);|\newline%
-\newline%
-\verb|pow_int :: forall a. (Group a) => Integer -> a -> a;|\newline%
-\verb|pow_int k x =|\newline%
-\verb|  (if 0 <= k then pow_nat (nat k) x|\newline%
-\verb|    else inverse (pow_nat (nat (negate k)) x));|\newline%
-\newline%
-\verb|example :: Integer;|\newline%
-\verb|example = pow_int 10 (-2);|\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}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
+\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
+\hspace*{0pt}\\
+\hspace*{0pt}nat ::~Integer -> Nat;\\
+\hspace*{0pt}nat i = nat{\char95}aux i 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) => Monoidl a where {\char123}\\
+\hspace*{0pt} ~neutral ::~a;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
+\hspace*{0pt} ~inverse ::~a -> a;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
+\hspace*{0pt}inverse{\char95}int i = negate i;\\
+\hspace*{0pt}\\
+\hspace*{0pt}neutral{\char95}int ::~Integer;\\
+\hspace*{0pt}neutral{\char95}int = 0;\\
+\hspace*{0pt}\\
+\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
+\hspace*{0pt}mult{\char95}int i j = i + j;\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Semigroup Integer where {\char123}\\
+\hspace*{0pt} ~mult = mult{\char95}int;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Monoidl Integer where {\char123}\\
+\hspace*{0pt} ~neutral = neutral{\char95}int;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Monoid Integer where {\char123}\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Group Integer where {\char123}\\
+\hspace*{0pt} ~inverse = inverse{\char95}int;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}pow{\char95}nat ::~forall a. (Monoid a) => Nat -> a -> a;\\
+\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
+\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
+\hspace*{0pt}\\
+\hspace*{0pt}pow{\char95}int ::~forall a. (Group a) => Integer -> a -> a;\\
+\hspace*{0pt}pow{\char95}int k x =\\
+\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
+\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
+\hspace*{0pt}\\
+\hspace*{0pt}example ::~Integer;\\
+\hspace*{0pt}example = pow{\char95}int 10 (-2);\\
+\hspace*{0pt}\\
+\hspace*{0pt}{\char125}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1203,64 +1203,64 @@
 \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 nat_aux i n =|\newline%
-\verb|  (if IntInf.<= (i, (0 : IntInf.int)) then n|\newline%
-\verb|    else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));|\newline%
-\newline%
-\verb|fun nat i = nat_aux i 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 monoidl =|\newline%
-\verb|  {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};|\newline%
-\verb|fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;|\newline%
-\verb|fun neutral (A_:'a monoidl) = #neutral A_;|\newline%
-\newline%
-\verb|type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};|\newline%
-\verb|fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;|\newline%
-\newline%
-\verb|type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};|\newline%
-\verb|fun monoid_group (A_:'a group) = #Classes__monoid_group A_;|\newline%
-\verb|fun inverse (A_:'a group) = #inverse A_;|\newline%
-\newline%
-\verb|fun inverse_int i = IntInf.~ i;|\newline%
-\newline%
-\verb|val neutral_int : IntInf.int = (0 : IntInf.int);|\newline%
-\newline%
-\verb|fun mult_int i j = IntInf.+ (i, j);|\newline%
-\newline%
-\verb|val semigroup_int = {mult = mult_int} : IntInf.int semigroup;|\newline%
-\newline%
-\verb|val monoidl_int =|\newline%
-\verb|  {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :|\newline%
-\verb|  IntInf.int monoidl;|\newline%
-\newline%
-\verb|val monoid_int = {Classes__monoidl_monoid = monoidl_int} :|\newline%
-\verb|  IntInf.int monoid;|\newline%
-\newline%
-\verb|val group_int =|\newline%
-\verb|  {Classes__monoid_group = monoid_int, inverse = inverse_int} :|\newline%
-\verb|  IntInf.int group;|\newline%
-\newline%
-\verb|fun pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_)|\newline%
-\verb|  |\verb,|,\verb| pow_nat A_ (Suc n) x =|\newline%
-\verb|    mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x);|\newline%
-\newline%
-\verb|fun pow_int A_ k x =|\newline%
-\verb|  (if IntInf.<= ((0 : IntInf.int), k)|\newline%
-\verb|    then pow_nat (monoid_group A_) (nat k) x|\newline%
-\verb|    else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));|\newline%
-\newline%
-\verb|val example : IntInf.int =|\newline%
-\verb|  pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);|\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 nat{\char95}aux i n =\\
+\hspace*{0pt} ~(if IntInf.<= (i, (0 :~IntInf.int)) then n\\
+\hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i, (1 :~IntInf.int))) (Suc n));\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun nat i = nat{\char95}aux i 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 monoidl =\\
+\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup, neutral :~'a{\char125};\\
+\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\
+\hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\
+\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid, inverse :~'a -> 'a{\char125};\\
+\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\
+\hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i, j);\\
+\hspace*{0pt}\\
+\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val monoidl{\char95}int =\\
+\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int, neutral = neutral{\char95}int{\char125}~:\\
+\hspace*{0pt} ~IntInf.int monoidl;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\
+\hspace*{0pt} ~IntInf.int monoid;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val group{\char95}int =\\
+\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int, inverse = inverse{\char95}int{\char125}~:\\
+\hspace*{0pt} ~IntInf.int group;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
+\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
+\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
+\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int), k)\\
+\hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
+\hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
+\hspace*{0pt}\\
+\hspace*{0pt}val example :~IntInf.int =\\
+\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
+\hspace*{0pt}\\
+\hspace*{0pt}end; (*struct Example*)%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 135317cd34d6 -r 1992553cccfe doc-src/IsarAdvanced/Classes/classes.tex
--- a/doc-src/IsarAdvanced/Classes/classes.tex	Fri Oct 31 10:39:04 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/classes.tex	Mon Nov 03 14:15:25 2008 +0100
@@ -24,7 +24,7 @@
 \newcommand{\qt}[1]{``{#1}''}
 
 % verbatim text
-\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
+\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
 
 % invisibility
 \isadroptag{theory}
diff -r 135317cd34d6 -r 1992553cccfe doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 31 10:39:04 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Mon Nov 03 14:15:25 2008 +0100
@@ -301,7 +301,7 @@
 *}
 
 code_class %quotett eq
-  (Haskell "Eq" where "HOL.eq" \<equiv> "(==)")
+  (Haskell "Eq")
 
 code_const %quotett "op ="
   (Haskell infixl 4 "==")
diff -r 135317cd34d6 -r 1992553cccfe doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 31 10:39:04 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Mon Nov 03 14:15:25 2008 +0100
@@ -264,26 +264,26 @@
 \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|datatype boola = False |\verb,|,\verb| True;|\newline%
-\newline%
-\verb|fun anda x True = x|\newline%
-\verb|  |\verb,|,\verb| anda x False = False|\newline%
-\verb|  |\verb,|,\verb| anda True x = x|\newline%
-\verb|  |\verb,|,\verb| anda False x = False;|\newline%
-\newline%
-\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
-\verb|  |\verb,|,\verb| less_nat n Zero_nat = False|\newline%
-\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
-\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = True;|\newline%
-\newline%
-\verb|fun in_interval (k, l) n = anda (less_eq_nat k n) (less_eq_nat n l);|\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}datatype boola = False | True;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun anda x True = x\\
+\hspace*{0pt} ~| anda x False = False\\
+\hspace*{0pt} ~| anda True x = x\\
+\hspace*{0pt} ~| anda False x = False;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
+\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun in{\char95}interval (k, l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}\\
+\hspace*{0pt}end; (*struct Example*)%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -347,19 +347,19 @@
 \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 less_nat m (Suc n) = less_eq_nat m n|\newline%
-\verb|  |\verb,|,\verb| less_nat n Zero_nat = false|\newline%
-\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
-\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline%
-\newline%
-\verb|fun in_interval (k, l) n = (less_eq_nat k n) andalso (less_eq_nat n l);|\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 less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
+\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun in{\char95}interval (k, l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
+\hspace*{0pt}\\
+\hspace*{0pt}end; (*struct Example*)%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -404,19 +404,19 @@
 \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 less_nat m (Suc n) = less_eq_nat m n|\newline%
-\verb|  |\verb,|,\verb| less_nat n Zero_nat = false|\newline%
-\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
-\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline%
-\newline%
-\verb|fun in_interval (k, l) n = less_eq_nat k n andalso less_eq_nat n l;|\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 less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
+\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
+\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun in{\char95}interval (k, l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
+\hspace*{0pt}\\
+\hspace*{0pt}end; (*struct Example*)%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -533,7 +533,7 @@
 \isatagquotett
 \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
 \ eq\isanewline
-\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}HOL{\isachardot}eq{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
diff -r 135317cd34d6 -r 1992553cccfe doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Fri Oct 31 10:39:04 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Mon Nov 03 14:15:25 2008 +0100
@@ -151,33 +151,33 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|structure Example = |\newline%
-\verb|struct|\newline%
-\newline%
-\verb|fun foldl f a [] = a|\newline%
-\verb|  |\verb,|,\verb| foldl f a (x :: xs) = foldl f (f a x) xs;|\newline%
-\newline%
-\verb|fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;|\newline%
-\newline%
-\verb|fun list_case f1 f2 (a :: lista) = f2 a lista|\newline%
-\verb|  |\verb,|,\verb| list_case f1 f2 [] = f1;|\newline%
-\newline%
-\verb|datatype 'a queue = Queue of 'a list * 'a list;|\newline%
-\newline%
-\verb|val empty : 'a queue = Queue ([], []);|\newline%
-\newline%
-\verb|fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))|\newline%
-\verb|  |\verb,|,\verb| dequeue (Queue (xs, y :: ys)) = (SOME y, Queue (xs, ys))|\newline%
-\verb|  |\verb,|,\verb| dequeue (Queue (v :: va, [])) =|\newline%
-\verb|    let|\newline%
-\verb|      val y :: ys = rev (v :: va);|\newline%
-\verb|    in|\newline%
-\verb|      (SOME y, Queue ([], ys))|\newline%
-\verb|    end;|\newline%
-\newline%
-\verb|fun enqueue x (Queue (xs, ys)) = Queue (x :: xs, ys);|\newline%
-\newline%
-\verb|end; (*struct Example*)|%
+\hspace*{0pt}structure Example = \\
+\hspace*{0pt}struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun foldl f a [] = a\\
+\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\
+\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype 'a queue = Queue of 'a list * 'a list;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val empty :~'a queue = Queue ([], []);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))\\
+\hspace*{0pt} ~| dequeue (Queue (xs, y ::~ys)) = (SOME y, Queue (xs, ys))\\
+\hspace*{0pt} ~| dequeue (Queue (v ::~va, [])) =\\
+\hspace*{0pt} ~~~let\\
+\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
+\hspace*{0pt} ~~~in\\
+\hspace*{0pt} ~~~~~(SOME y, Queue ([], ys))\\
+\hspace*{0pt} ~~~end;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun enqueue x (Queue (xs, ys)) = Queue (x ::~xs, ys);\\
+\hspace*{0pt}\\
+\hspace*{0pt}end; (*struct Example*)%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -230,37 +230,37 @@
 \begin{isamarkuptext}%
 \isaverbatim%
 \noindent%
-\verb|module Example where {|\newline%
-\newline%
-\newline%
-\verb|foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;|\newline%
-\verb|foldla f a [] = a;|\newline%
-\verb|foldla f a (x : xs) = foldla f (f a x) xs;|\newline%
-\newline%
-\verb|rev :: forall a. [a] -> [a];|\newline%
-\verb|rev xs = foldla (\ xsa x -> x : xsa) [] xs;|\newline%
-\newline%
-\verb|list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;|\newline%
-\verb|list_case f1 f2 (a : list) = f2 a list;|\newline%
-\verb|list_case f1 f2 [] = f1;|\newline%
-\newline%
-\verb|data Queue a = Queue [a] [a];|\newline%
-\newline%
-\verb|empty :: forall a. Queue a;|\newline%
-\verb|empty = Queue [] [];|\newline%
-\newline%
-\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline%
-\verb|dequeue (Queue [] []) = (Nothing, Queue [] []);|\newline%
-\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline%
-\verb|dequeue (Queue (v : va) []) =|\newline%
-\verb|  let {|\newline%
-\verb|    (y : ys) = rev (v : va);|\newline%
-\verb|  } in (Just y, Queue [] ys);|\newline%
-\newline%
-\verb|enqueue :: forall a. a -> Queue a -> Queue a;|\newline%
-\verb|enqueue x (Queue xs ys) = Queue (x : xs) ys;|\newline%
-\newline%
-\verb|}|%
+\hspace*{0pt}module Example where {\char123}\\
+\hspace*{0pt}\\
+\hspace*{0pt}\\
+\hspace*{0pt}foldla ::~forall a b. (a -> b -> a) -> a -> [b] -> a;\\
+\hspace*{0pt}foldla f a [] = a;\\
+\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}rev ::~forall a. [a] -> [a];\\
+\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}list{\char95}case ::~forall t a. t -> (a -> [a] -> t) -> [a] -> t;\\
+\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
+\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
+\hspace*{0pt}\\
+\hspace*{0pt}data Queue a = Queue [a] [a];\\
+\hspace*{0pt}\\
+\hspace*{0pt}empty ::~forall a. Queue a;\\
+\hspace*{0pt}empty = Queue [] [];\\
+\hspace*{0pt}\\
+\hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\
+\hspace*{0pt}dequeue (Queue [] []) = (Nothing, Queue [] []);\\
+\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\
+\hspace*{0pt}dequeue (Queue (v :~va) []) =\\
+\hspace*{0pt} ~let {\char123}\\
+\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
+\hspace*{0pt} ~{\char125}~in (Just y, Queue [] ys);\\
+\hspace*{0pt}\\
+\hspace*{0pt}enqueue ::~forall a. a -> Queue a -> Queue a;\\
+\hspace*{0pt}enqueue x (Queue xs ys) = Queue (x :~xs) ys;\\
+\hspace*{0pt}\\
+\hspace*{0pt}{\char125}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
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%
 %
diff -r 135317cd34d6 -r 1992553cccfe doc-src/IsarAdvanced/Codegen/codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Fri Oct 31 10:39:04 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Nov 03 14:15:25 2008 +0100
@@ -26,7 +26,7 @@
 \newcommand{\qt}[1]{``{#1}''}
 
 % verbatim text
-\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
+\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
 
 % invisibility
 \isadroptag{theory}
diff -r 135317cd34d6 -r 1992553cccfe doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Fri Oct 31 10:39:04 2008 +0100
+++ b/doc-src/more_antiquote.ML	Mon Nov 03 14:15:25 2008 +0100
@@ -7,7 +7,7 @@
 
 signature MORE_ANTIQUOTE =
 sig
-  val verbatim_lines: string list -> string
+  val verbatim: string -> string
 end;
 
 structure More_Antiquote : MORE_ANTIQUOTE =
@@ -17,12 +17,34 @@
 
 (* printing verbatim lines *)
 
-val verbatim_line = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
-val verbatim_lines = rev
-  #> dropwhile (fn s => s = "")
-  #> rev
-  #> map verbatim_line #> space_implode "\\newline%\n"
-  #> prefix "\\isaverbatim%\n\\noindent%\n"
+fun verbatim s =
+  let
+    val parse = Scan.repeat
+      (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
+        || (Scan.this_string " " 
+          || Scan.this_string ":"
+          || Scan.this_string "\"" |-- Scan.succeed "{\\char34}"
+          || Scan.this_string "#" |-- Scan.succeed "{\\char35}"
+          || Scan.this_string "$" |-- Scan.succeed "{\\char36}"
+          || Scan.this_string "%" |-- Scan.succeed "{\\char37}"
+          || Scan.this_string "&" |-- Scan.succeed "{\\char38}"
+          || Scan.this_string "\\" |-- Scan.succeed "{\\char92}"
+          || Scan.this_string "^" |-- Scan.succeed "{\\char94}"
+          || Scan.this_string "_" |-- Scan.succeed "{\\char95}"
+          || Scan.this_string "{" |-- Scan.succeed "{\\char123}"
+          || Scan.this_string "}" |-- Scan.succeed "{\\char125}"
+          || Scan.this_string "~" |-- Scan.succeed "{\\char126}")
+          -- Scan.repeat (Scan.this_string " ")
+          >> (fn (x, xs) => x ^ replicate_string (length xs) "~")
+        || Scan.one Symbol.not_eof);
+    fun is_newline s = (s = "\n");
+    val cs = explode s |> take_prefix is_newline |> snd
+      |> take_suffix is_newline |> fst;
+    val (texts, []) =  Scan.finite Symbol.stopper parse cs
+  in if null texts
+    then ""
+    else implode ("\\isaverbatim%\n\\noindent%\n\\hspace*{0pt}" :: texts)
+  end
 
 
 (* class antiquotation *)
@@ -69,8 +91,7 @@
     Code_Target.code_of (ProofContext.theory_of ctxt)
       target "Example" (mk_cs (ProofContext.theory_of ctxt))
         (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
-    |> split_lines
-    |> verbatim_lines;
+    |> verbatim;
 
 in