improved verbatim mechanism
authorhaftmann
Mon Nov 03 14:15:25 2008 +0100 (2008-11-03)
changeset 287141992553cccfe
parent 28713 135317cd34d6
child 28715 238f9966c80e
improved verbatim mechanism
doc-src/IsarAdvanced/Classes/IsaMakefile
doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
doc-src/IsarAdvanced/Classes/classes.tex
doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex
doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
doc-src/IsarAdvanced/Codegen/codegen.tex
doc-src/more_antiquote.ML
     1.1 --- a/doc-src/IsarAdvanced/Classes/IsaMakefile	Fri Oct 31 10:39:04 2008 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Classes/IsaMakefile	Mon Nov 03 14:15:25 2008 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5  Thy: $(THY)
     1.6  
     1.7 -$(THY): Thy/ROOT.ML Thy/Classes.thy
     1.8 +$(THY): Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy
     1.9  	@$(USEDIR) HOL Thy
    1.10  
    1.11  
     2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 31 10:39:04 2008 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Mon Nov 03 14:15:25 2008 +0100
     2.3 @@ -1116,69 +1116,69 @@
     2.4  \begin{isamarkuptext}%
     2.5  \isaverbatim%
     2.6  \noindent%
     2.7 -\verb|module Example where {|\newline%
     2.8 -\newline%
     2.9 -\newline%
    2.10 -\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
    2.11 -\newline%
    2.12 -\verb|nat_aux :: Integer -> Nat -> Nat;|\newline%
    2.13 -\verb|nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));|\newline%
    2.14 -\newline%
    2.15 -\verb|nat :: Integer -> Nat;|\newline%
    2.16 -\verb|nat i = nat_aux i Zero_nat;|\newline%
    2.17 -\newline%
    2.18 -\verb|class Semigroup a where {|\newline%
    2.19 -\verb|  mult :: a -> a -> a;|\newline%
    2.20 -\verb|};|\newline%
    2.21 -\newline%
    2.22 -\verb|class (Semigroup a) => Monoidl a where {|\newline%
    2.23 -\verb|  neutral :: a;|\newline%
    2.24 -\verb|};|\newline%
    2.25 -\newline%
    2.26 -\verb|class (Monoidl a) => Monoid a where {|\newline%
    2.27 -\verb|};|\newline%
    2.28 -\newline%
    2.29 -\verb|class (Monoid a) => Group a where {|\newline%
    2.30 -\verb|  inverse :: a -> a;|\newline%
    2.31 -\verb|};|\newline%
    2.32 -\newline%
    2.33 -\verb|inverse_int :: Integer -> Integer;|\newline%
    2.34 -\verb|inverse_int i = negate i;|\newline%
    2.35 -\newline%
    2.36 -\verb|neutral_int :: Integer;|\newline%
    2.37 -\verb|neutral_int = 0;|\newline%
    2.38 -\newline%
    2.39 -\verb|mult_int :: Integer -> Integer -> Integer;|\newline%
    2.40 -\verb|mult_int i j = i + j;|\newline%
    2.41 -\newline%
    2.42 -\verb|instance Semigroup Integer where {|\newline%
    2.43 -\verb|  mult = mult_int;|\newline%
    2.44 -\verb|};|\newline%
    2.45 -\newline%
    2.46 -\verb|instance Monoidl Integer where {|\newline%
    2.47 -\verb|  neutral = neutral_int;|\newline%
    2.48 -\verb|};|\newline%
    2.49 -\newline%
    2.50 -\verb|instance Monoid Integer where {|\newline%
    2.51 -\verb|};|\newline%
    2.52 -\newline%
    2.53 -\verb|instance Group Integer where {|\newline%
    2.54 -\verb|  inverse = inverse_int;|\newline%
    2.55 -\verb|};|\newline%
    2.56 -\newline%
    2.57 -\verb|pow_nat :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
    2.58 -\verb|pow_nat Zero_nat x = neutral;|\newline%
    2.59 -\verb|pow_nat (Suc n) x = mult x (pow_nat n x);|\newline%
    2.60 -\newline%
    2.61 -\verb|pow_int :: forall a. (Group a) => Integer -> a -> a;|\newline%
    2.62 -\verb|pow_int k x =|\newline%
    2.63 -\verb|  (if 0 <= k then pow_nat (nat k) x|\newline%
    2.64 -\verb|    else inverse (pow_nat (nat (negate k)) x));|\newline%
    2.65 -\newline%
    2.66 -\verb|example :: Integer;|\newline%
    2.67 -\verb|example = pow_int 10 (-2);|\newline%
    2.68 -\newline%
    2.69 -\verb|}|%
    2.70 +\hspace*{0pt}module Example where {\char123}\\
    2.71 +\hspace*{0pt}\\
    2.72 +\hspace*{0pt}\\
    2.73 +\hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
    2.74 +\hspace*{0pt}\\
    2.75 +\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
    2.76 +\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
    2.77 +\hspace*{0pt}\\
    2.78 +\hspace*{0pt}nat ::~Integer -> Nat;\\
    2.79 +\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
    2.80 +\hspace*{0pt}\\
    2.81 +\hspace*{0pt}class Semigroup a where {\char123}\\
    2.82 +\hspace*{0pt} ~mult ::~a -> a -> a;\\
    2.83 +\hspace*{0pt}{\char125};\\
    2.84 +\hspace*{0pt}\\
    2.85 +\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
    2.86 +\hspace*{0pt} ~neutral ::~a;\\
    2.87 +\hspace*{0pt}{\char125};\\
    2.88 +\hspace*{0pt}\\
    2.89 +\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
    2.90 +\hspace*{0pt}{\char125};\\
    2.91 +\hspace*{0pt}\\
    2.92 +\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
    2.93 +\hspace*{0pt} ~inverse ::~a -> a;\\
    2.94 +\hspace*{0pt}{\char125};\\
    2.95 +\hspace*{0pt}\\
    2.96 +\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
    2.97 +\hspace*{0pt}inverse{\char95}int i = negate i;\\
    2.98 +\hspace*{0pt}\\
    2.99 +\hspace*{0pt}neutral{\char95}int ::~Integer;\\
   2.100 +\hspace*{0pt}neutral{\char95}int = 0;\\
   2.101 +\hspace*{0pt}\\
   2.102 +\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
   2.103 +\hspace*{0pt}mult{\char95}int i j = i + j;\\
   2.104 +\hspace*{0pt}\\
   2.105 +\hspace*{0pt}instance Semigroup Integer where {\char123}\\
   2.106 +\hspace*{0pt} ~mult = mult{\char95}int;\\
   2.107 +\hspace*{0pt}{\char125};\\
   2.108 +\hspace*{0pt}\\
   2.109 +\hspace*{0pt}instance Monoidl Integer where {\char123}\\
   2.110 +\hspace*{0pt} ~neutral = neutral{\char95}int;\\
   2.111 +\hspace*{0pt}{\char125};\\
   2.112 +\hspace*{0pt}\\
   2.113 +\hspace*{0pt}instance Monoid Integer where {\char123}\\
   2.114 +\hspace*{0pt}{\char125};\\
   2.115 +\hspace*{0pt}\\
   2.116 +\hspace*{0pt}instance Group Integer where {\char123}\\
   2.117 +\hspace*{0pt} ~inverse = inverse{\char95}int;\\
   2.118 +\hspace*{0pt}{\char125};\\
   2.119 +\hspace*{0pt}\\
   2.120 +\hspace*{0pt}pow{\char95}nat ::~forall a. (Monoid a) => Nat -> a -> a;\\
   2.121 +\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
   2.122 +\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
   2.123 +\hspace*{0pt}\\
   2.124 +\hspace*{0pt}pow{\char95}int ::~forall a. (Group a) => Integer -> a -> a;\\
   2.125 +\hspace*{0pt}pow{\char95}int k x =\\
   2.126 +\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
   2.127 +\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
   2.128 +\hspace*{0pt}\\
   2.129 +\hspace*{0pt}example ::~Integer;\\
   2.130 +\hspace*{0pt}example = pow{\char95}int 10 (-2);\\
   2.131 +\hspace*{0pt}\\
   2.132 +\hspace*{0pt}{\char125}%
   2.133  \end{isamarkuptext}%
   2.134  \isamarkuptrue%
   2.135  %
   2.136 @@ -1203,64 +1203,64 @@
   2.137  \begin{isamarkuptext}%
   2.138  \isaverbatim%
   2.139  \noindent%
   2.140 -\verb|structure Example = |\newline%
   2.141 -\verb|struct|\newline%
   2.142 -\newline%
   2.143 -\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
   2.144 -\newline%
   2.145 -\verb|fun nat_aux i n =|\newline%
   2.146 -\verb|  (if IntInf.<= (i, (0 : IntInf.int)) then n|\newline%
   2.147 -\verb|    else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));|\newline%
   2.148 -\newline%
   2.149 -\verb|fun nat i = nat_aux i Zero_nat;|\newline%
   2.150 -\newline%
   2.151 -\verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline%
   2.152 -\verb|fun mult (A_:'a semigroup) = #mult A_;|\newline%
   2.153 -\newline%
   2.154 -\verb|type 'a monoidl =|\newline%
   2.155 -\verb|  {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};|\newline%
   2.156 -\verb|fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;|\newline%
   2.157 -\verb|fun neutral (A_:'a monoidl) = #neutral A_;|\newline%
   2.158 -\newline%
   2.159 -\verb|type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};|\newline%
   2.160 -\verb|fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;|\newline%
   2.161 -\newline%
   2.162 -\verb|type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};|\newline%
   2.163 -\verb|fun monoid_group (A_:'a group) = #Classes__monoid_group A_;|\newline%
   2.164 -\verb|fun inverse (A_:'a group) = #inverse A_;|\newline%
   2.165 -\newline%
   2.166 -\verb|fun inverse_int i = IntInf.~ i;|\newline%
   2.167 -\newline%
   2.168 -\verb|val neutral_int : IntInf.int = (0 : IntInf.int);|\newline%
   2.169 -\newline%
   2.170 -\verb|fun mult_int i j = IntInf.+ (i, j);|\newline%
   2.171 -\newline%
   2.172 -\verb|val semigroup_int = {mult = mult_int} : IntInf.int semigroup;|\newline%
   2.173 -\newline%
   2.174 -\verb|val monoidl_int =|\newline%
   2.175 -\verb|  {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :|\newline%
   2.176 -\verb|  IntInf.int monoidl;|\newline%
   2.177 -\newline%
   2.178 -\verb|val monoid_int = {Classes__monoidl_monoid = monoidl_int} :|\newline%
   2.179 -\verb|  IntInf.int monoid;|\newline%
   2.180 -\newline%
   2.181 -\verb|val group_int =|\newline%
   2.182 -\verb|  {Classes__monoid_group = monoid_int, inverse = inverse_int} :|\newline%
   2.183 -\verb|  IntInf.int group;|\newline%
   2.184 -\newline%
   2.185 -\verb|fun pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_)|\newline%
   2.186 -\verb|  |\verb,|,\verb| pow_nat A_ (Suc n) x =|\newline%
   2.187 -\verb|    mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x);|\newline%
   2.188 -\newline%
   2.189 -\verb|fun pow_int A_ k x =|\newline%
   2.190 -\verb|  (if IntInf.<= ((0 : IntInf.int), k)|\newline%
   2.191 -\verb|    then pow_nat (monoid_group A_) (nat k) x|\newline%
   2.192 -\verb|    else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));|\newline%
   2.193 -\newline%
   2.194 -\verb|val example : IntInf.int =|\newline%
   2.195 -\verb|  pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);|\newline%
   2.196 -\newline%
   2.197 -\verb|end; (*struct Example*)|%
   2.198 +\hspace*{0pt}structure Example = \\
   2.199 +\hspace*{0pt}struct\\
   2.200 +\hspace*{0pt}\\
   2.201 +\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
   2.202 +\hspace*{0pt}\\
   2.203 +\hspace*{0pt}fun nat{\char95}aux i n =\\
   2.204 +\hspace*{0pt} ~(if IntInf.<= (i, (0 :~IntInf.int)) then n\\
   2.205 +\hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i, (1 :~IntInf.int))) (Suc n));\\
   2.206 +\hspace*{0pt}\\
   2.207 +\hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\
   2.208 +\hspace*{0pt}\\
   2.209 +\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
   2.210 +\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
   2.211 +\hspace*{0pt}\\
   2.212 +\hspace*{0pt}type 'a monoidl =\\
   2.213 +\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup, neutral :~'a{\char125};\\
   2.214 +\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\
   2.215 +\hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
   2.216 +\hspace*{0pt}\\
   2.217 +\hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\
   2.218 +\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\
   2.219 +\hspace*{0pt}\\
   2.220 +\hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid, inverse :~'a -> 'a{\char125};\\
   2.221 +\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\
   2.222 +\hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
   2.223 +\hspace*{0pt}\\
   2.224 +\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
   2.225 +\hspace*{0pt}\\
   2.226 +\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
   2.227 +\hspace*{0pt}\\
   2.228 +\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i, j);\\
   2.229 +\hspace*{0pt}\\
   2.230 +\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
   2.231 +\hspace*{0pt}\\
   2.232 +\hspace*{0pt}val monoidl{\char95}int =\\
   2.233 +\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int, neutral = neutral{\char95}int{\char125}~:\\
   2.234 +\hspace*{0pt} ~IntInf.int monoidl;\\
   2.235 +\hspace*{0pt}\\
   2.236 +\hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\
   2.237 +\hspace*{0pt} ~IntInf.int monoid;\\
   2.238 +\hspace*{0pt}\\
   2.239 +\hspace*{0pt}val group{\char95}int =\\
   2.240 +\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int, inverse = inverse{\char95}int{\char125}~:\\
   2.241 +\hspace*{0pt} ~IntInf.int group;\\
   2.242 +\hspace*{0pt}\\
   2.243 +\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
   2.244 +\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
   2.245 +\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
   2.246 +\hspace*{0pt}\\
   2.247 +\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
   2.248 +\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int), k)\\
   2.249 +\hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
   2.250 +\hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
   2.251 +\hspace*{0pt}\\
   2.252 +\hspace*{0pt}val example :~IntInf.int =\\
   2.253 +\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
   2.254 +\hspace*{0pt}\\
   2.255 +\hspace*{0pt}end; (*struct Example*)%
   2.256  \end{isamarkuptext}%
   2.257  \isamarkuptrue%
   2.258  %
     3.1 --- a/doc-src/IsarAdvanced/Classes/classes.tex	Fri Oct 31 10:39:04 2008 +0100
     3.2 +++ b/doc-src/IsarAdvanced/Classes/classes.tex	Mon Nov 03 14:15:25 2008 +0100
     3.3 @@ -24,7 +24,7 @@
     3.4  \newcommand{\qt}[1]{``{#1}''}
     3.5  
     3.6  % verbatim text
     3.7 -\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
     3.8 +\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
     3.9  
    3.10  % invisibility
    3.11  \isadroptag{theory}
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 31 10:39:04 2008 +0100
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Mon Nov 03 14:15:25 2008 +0100
     4.3 @@ -301,7 +301,7 @@
     4.4  *}
     4.5  
     4.6  code_class %quotett eq
     4.7 -  (Haskell "Eq" where "HOL.eq" \<equiv> "(==)")
     4.8 +  (Haskell "Eq")
     4.9  
    4.10  code_const %quotett "op ="
    4.11    (Haskell infixl 4 "==")
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 31 10:39:04 2008 +0100
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Mon Nov 03 14:15:25 2008 +0100
     5.3 @@ -264,26 +264,26 @@
     5.4  \begin{isamarkuptext}%
     5.5  \isaverbatim%
     5.6  \noindent%
     5.7 -\verb|structure Example = |\newline%
     5.8 -\verb|struct|\newline%
     5.9 -\newline%
    5.10 -\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
    5.11 -\newline%
    5.12 -\verb|datatype boola = False |\verb,|,\verb| True;|\newline%
    5.13 -\newline%
    5.14 -\verb|fun anda x True = x|\newline%
    5.15 -\verb|  |\verb,|,\verb| anda x False = False|\newline%
    5.16 -\verb|  |\verb,|,\verb| anda True x = x|\newline%
    5.17 -\verb|  |\verb,|,\verb| anda False x = False;|\newline%
    5.18 -\newline%
    5.19 -\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
    5.20 -\verb|  |\verb,|,\verb| less_nat n Zero_nat = False|\newline%
    5.21 -\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
    5.22 -\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = True;|\newline%
    5.23 -\newline%
    5.24 -\verb|fun in_interval (k, l) n = anda (less_eq_nat k n) (less_eq_nat n l);|\newline%
    5.25 -\newline%
    5.26 -\verb|end; (*struct Example*)|%
    5.27 +\hspace*{0pt}structure Example = \\
    5.28 +\hspace*{0pt}struct\\
    5.29 +\hspace*{0pt}\\
    5.30 +\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    5.31 +\hspace*{0pt}\\
    5.32 +\hspace*{0pt}datatype boola = False | True;\\
    5.33 +\hspace*{0pt}\\
    5.34 +\hspace*{0pt}fun anda x True = x\\
    5.35 +\hspace*{0pt} ~| anda x False = False\\
    5.36 +\hspace*{0pt} ~| anda True x = x\\
    5.37 +\hspace*{0pt} ~| anda False x = False;\\
    5.38 +\hspace*{0pt}\\
    5.39 +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
    5.40 +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
    5.41 +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
    5.42 +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
    5.43 +\hspace*{0pt}\\
    5.44 +\hspace*{0pt}fun in{\char95}interval (k, l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
    5.45 +\hspace*{0pt}\\
    5.46 +\hspace*{0pt}end; (*struct Example*)%
    5.47  \end{isamarkuptext}%
    5.48  \isamarkuptrue%
    5.49  %
    5.50 @@ -347,19 +347,19 @@
    5.51  \begin{isamarkuptext}%
    5.52  \isaverbatim%
    5.53  \noindent%
    5.54 -\verb|structure Example = |\newline%
    5.55 -\verb|struct|\newline%
    5.56 -\newline%
    5.57 -\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
    5.58 -\newline%
    5.59 -\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
    5.60 -\verb|  |\verb,|,\verb| less_nat n Zero_nat = false|\newline%
    5.61 -\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
    5.62 -\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline%
    5.63 -\newline%
    5.64 -\verb|fun in_interval (k, l) n = (less_eq_nat k n) andalso (less_eq_nat n l);|\newline%
    5.65 -\newline%
    5.66 -\verb|end; (*struct Example*)|%
    5.67 +\hspace*{0pt}structure Example = \\
    5.68 +\hspace*{0pt}struct\\
    5.69 +\hspace*{0pt}\\
    5.70 +\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
    5.71 +\hspace*{0pt}\\
    5.72 +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
    5.73 +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
    5.74 +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
    5.75 +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
    5.76 +\hspace*{0pt}\\
    5.77 +\hspace*{0pt}fun in{\char95}interval (k, l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
    5.78 +\hspace*{0pt}\\
    5.79 +\hspace*{0pt}end; (*struct Example*)%
    5.80  \end{isamarkuptext}%
    5.81  \isamarkuptrue%
    5.82  %
    5.83 @@ -404,19 +404,19 @@
    5.84  \begin{isamarkuptext}%
    5.85  \isaverbatim%
    5.86  \noindent%
    5.87 -\verb|structure Example = |\newline%
    5.88 -\verb|struct|\newline%
    5.89 -\newline%
    5.90 -\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
    5.91 -\newline%
    5.92 -\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
    5.93 -\verb|  |\verb,|,\verb| less_nat n Zero_nat = false|\newline%
    5.94 -\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
    5.95 -\verb|  |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline%
    5.96 -\newline%
    5.97 -\verb|fun in_interval (k, l) n = less_eq_nat k n andalso less_eq_nat n l;|\newline%
    5.98 -\newline%
    5.99 -\verb|end; (*struct Example*)|%
   5.100 +\hspace*{0pt}structure Example = \\
   5.101 +\hspace*{0pt}struct\\
   5.102 +\hspace*{0pt}\\
   5.103 +\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
   5.104 +\hspace*{0pt}\\
   5.105 +\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
   5.106 +\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
   5.107 +\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
   5.108 +\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
   5.109 +\hspace*{0pt}\\
   5.110 +\hspace*{0pt}fun in{\char95}interval (k, l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
   5.111 +\hspace*{0pt}\\
   5.112 +\hspace*{0pt}end; (*struct Example*)%
   5.113  \end{isamarkuptext}%
   5.114  \isamarkuptrue%
   5.115  %
   5.116 @@ -533,7 +533,7 @@
   5.117  \isatagquotett
   5.118  \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
   5.119  \ eq\isanewline
   5.120 -\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}HOL{\isachardot}eq{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   5.121 +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
   5.122  \isanewline
   5.123  \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
   5.124  \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Fri Oct 31 10:39:04 2008 +0100
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Mon Nov 03 14:15:25 2008 +0100
     6.3 @@ -151,33 +151,33 @@
     6.4  \begin{isamarkuptext}%
     6.5  \isaverbatim%
     6.6  \noindent%
     6.7 -\verb|structure Example = |\newline%
     6.8 -\verb|struct|\newline%
     6.9 -\newline%
    6.10 -\verb|fun foldl f a [] = a|\newline%
    6.11 -\verb|  |\verb,|,\verb| foldl f a (x :: xs) = foldl f (f a x) xs;|\newline%
    6.12 -\newline%
    6.13 -\verb|fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;|\newline%
    6.14 -\newline%
    6.15 -\verb|fun list_case f1 f2 (a :: lista) = f2 a lista|\newline%
    6.16 -\verb|  |\verb,|,\verb| list_case f1 f2 [] = f1;|\newline%
    6.17 -\newline%
    6.18 -\verb|datatype 'a queue = Queue of 'a list * 'a list;|\newline%
    6.19 -\newline%
    6.20 -\verb|val empty : 'a queue = Queue ([], []);|\newline%
    6.21 -\newline%
    6.22 -\verb|fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))|\newline%
    6.23 -\verb|  |\verb,|,\verb| dequeue (Queue (xs, y :: ys)) = (SOME y, Queue (xs, ys))|\newline%
    6.24 -\verb|  |\verb,|,\verb| dequeue (Queue (v :: va, [])) =|\newline%
    6.25 -\verb|    let|\newline%
    6.26 -\verb|      val y :: ys = rev (v :: va);|\newline%
    6.27 -\verb|    in|\newline%
    6.28 -\verb|      (SOME y, Queue ([], ys))|\newline%
    6.29 -\verb|    end;|\newline%
    6.30 -\newline%
    6.31 -\verb|fun enqueue x (Queue (xs, ys)) = Queue (x :: xs, ys);|\newline%
    6.32 -\newline%
    6.33 -\verb|end; (*struct Example*)|%
    6.34 +\hspace*{0pt}structure Example = \\
    6.35 +\hspace*{0pt}struct\\
    6.36 +\hspace*{0pt}\\
    6.37 +\hspace*{0pt}fun foldl f a [] = a\\
    6.38 +\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
    6.39 +\hspace*{0pt}\\
    6.40 +\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
    6.41 +\hspace*{0pt}\\
    6.42 +\hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\
    6.43 +\hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\
    6.44 +\hspace*{0pt}\\
    6.45 +\hspace*{0pt}datatype 'a queue = Queue of 'a list * 'a list;\\
    6.46 +\hspace*{0pt}\\
    6.47 +\hspace*{0pt}val empty :~'a queue = Queue ([], []);\\
    6.48 +\hspace*{0pt}\\
    6.49 +\hspace*{0pt}fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))\\
    6.50 +\hspace*{0pt} ~| dequeue (Queue (xs, y ::~ys)) = (SOME y, Queue (xs, ys))\\
    6.51 +\hspace*{0pt} ~| dequeue (Queue (v ::~va, [])) =\\
    6.52 +\hspace*{0pt} ~~~let\\
    6.53 +\hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
    6.54 +\hspace*{0pt} ~~~in\\
    6.55 +\hspace*{0pt} ~~~~~(SOME y, Queue ([], ys))\\
    6.56 +\hspace*{0pt} ~~~end;\\
    6.57 +\hspace*{0pt}\\
    6.58 +\hspace*{0pt}fun enqueue x (Queue (xs, ys)) = Queue (x ::~xs, ys);\\
    6.59 +\hspace*{0pt}\\
    6.60 +\hspace*{0pt}end; (*struct Example*)%
    6.61  \end{isamarkuptext}%
    6.62  \isamarkuptrue%
    6.63  %
    6.64 @@ -230,37 +230,37 @@
    6.65  \begin{isamarkuptext}%
    6.66  \isaverbatim%
    6.67  \noindent%
    6.68 -\verb|module Example where {|\newline%
    6.69 -\newline%
    6.70 -\newline%
    6.71 -\verb|foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;|\newline%
    6.72 -\verb|foldla f a [] = a;|\newline%
    6.73 -\verb|foldla f a (x : xs) = foldla f (f a x) xs;|\newline%
    6.74 -\newline%
    6.75 -\verb|rev :: forall a. [a] -> [a];|\newline%
    6.76 -\verb|rev xs = foldla (\ xsa x -> x : xsa) [] xs;|\newline%
    6.77 -\newline%
    6.78 -\verb|list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;|\newline%
    6.79 -\verb|list_case f1 f2 (a : list) = f2 a list;|\newline%
    6.80 -\verb|list_case f1 f2 [] = f1;|\newline%
    6.81 -\newline%
    6.82 -\verb|data Queue a = Queue [a] [a];|\newline%
    6.83 -\newline%
    6.84 -\verb|empty :: forall a. Queue a;|\newline%
    6.85 -\verb|empty = Queue [] [];|\newline%
    6.86 -\newline%
    6.87 -\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline%
    6.88 -\verb|dequeue (Queue [] []) = (Nothing, Queue [] []);|\newline%
    6.89 -\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline%
    6.90 -\verb|dequeue (Queue (v : va) []) =|\newline%
    6.91 -\verb|  let {|\newline%
    6.92 -\verb|    (y : ys) = rev (v : va);|\newline%
    6.93 -\verb|  } in (Just y, Queue [] ys);|\newline%
    6.94 -\newline%
    6.95 -\verb|enqueue :: forall a. a -> Queue a -> Queue a;|\newline%
    6.96 -\verb|enqueue x (Queue xs ys) = Queue (x : xs) ys;|\newline%
    6.97 -\newline%
    6.98 -\verb|}|%
    6.99 +\hspace*{0pt}module Example where {\char123}\\
   6.100 +\hspace*{0pt}\\
   6.101 +\hspace*{0pt}\\
   6.102 +\hspace*{0pt}foldla ::~forall a b. (a -> b -> a) -> a -> [b] -> a;\\
   6.103 +\hspace*{0pt}foldla f a [] = a;\\
   6.104 +\hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\
   6.105 +\hspace*{0pt}\\
   6.106 +\hspace*{0pt}rev ::~forall a. [a] -> [a];\\
   6.107 +\hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\
   6.108 +\hspace*{0pt}\\
   6.109 +\hspace*{0pt}list{\char95}case ::~forall t a. t -> (a -> [a] -> t) -> [a] -> t;\\
   6.110 +\hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
   6.111 +\hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
   6.112 +\hspace*{0pt}\\
   6.113 +\hspace*{0pt}data Queue a = Queue [a] [a];\\
   6.114 +\hspace*{0pt}\\
   6.115 +\hspace*{0pt}empty ::~forall a. Queue a;\\
   6.116 +\hspace*{0pt}empty = Queue [] [];\\
   6.117 +\hspace*{0pt}\\
   6.118 +\hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\
   6.119 +\hspace*{0pt}dequeue (Queue [] []) = (Nothing, Queue [] []);\\
   6.120 +\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\
   6.121 +\hspace*{0pt}dequeue (Queue (v :~va) []) =\\
   6.122 +\hspace*{0pt} ~let {\char123}\\
   6.123 +\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
   6.124 +\hspace*{0pt} ~{\char125}~in (Just y, Queue [] ys);\\
   6.125 +\hspace*{0pt}\\
   6.126 +\hspace*{0pt}enqueue ::~forall a. a -> Queue a -> Queue a;\\
   6.127 +\hspace*{0pt}enqueue x (Queue xs ys) = Queue (x :~xs) ys;\\
   6.128 +\hspace*{0pt}\\
   6.129 +\hspace*{0pt}{\char125}%
   6.130  \end{isamarkuptext}%
   6.131  \isamarkuptrue%
   6.132  %
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Fri Oct 31 10:39:04 2008 +0100
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Mon Nov 03 14:15:25 2008 +0100
     7.3 @@ -87,11 +87,11 @@
     7.4  \begin{isamarkuptext}%
     7.5  \isaverbatim%
     7.6  \noindent%
     7.7 -\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline%
     7.8 -\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline%
     7.9 -\verb|dequeue (Queue xs []) =|\newline%
    7.10 -\verb|  (if nulla xs then (Nothing, Queue [] [])|\newline%
    7.11 -\verb|    else dequeue (Queue [] (rev xs)));|%
    7.12 +\hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\
    7.13 +\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\
    7.14 +\hspace*{0pt}dequeue (Queue xs []) =\\
    7.15 +\hspace*{0pt} ~(if nulla xs then (Nothing, Queue [] [])\\
    7.16 +\hspace*{0pt} ~~~else dequeue (Queue [] (rev xs)));%
    7.17  \end{isamarkuptext}%
    7.18  \isamarkuptrue%
    7.19  %
    7.20 @@ -273,46 +273,46 @@
    7.21  \begin{isamarkuptext}%
    7.22  \isaverbatim%
    7.23  \noindent%
    7.24 -\verb|module Example where {|\newline%
    7.25 -\newline%
    7.26 -\newline%
    7.27 -\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
    7.28 -\newline%
    7.29 -\verb|class Semigroup a where {|\newline%
    7.30 -\verb|  mult :: a -> a -> a;|\newline%
    7.31 -\verb|};|\newline%
    7.32 -\newline%
    7.33 -\verb|class (Semigroup a) => Monoid a where {|\newline%
    7.34 -\verb|  neutral :: a;|\newline%
    7.35 -\verb|};|\newline%
    7.36 -\newline%
    7.37 -\verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
    7.38 -\verb|pow Zero_nat a = neutral;|\newline%
    7.39 -\verb|pow (Suc n) a = mult a (pow n a);|\newline%
    7.40 -\newline%
    7.41 -\verb|plus_nat :: Nat -> Nat -> Nat;|\newline%
    7.42 -\verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline%
    7.43 -\verb|plus_nat Zero_nat n = n;|\newline%
    7.44 -\newline%
    7.45 -\verb|neutral_nat :: Nat;|\newline%
    7.46 -\verb|neutral_nat = Suc Zero_nat;|\newline%
    7.47 -\newline%
    7.48 -\verb|mult_nat :: Nat -> Nat -> Nat;|\newline%
    7.49 -\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
    7.50 -\verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
    7.51 -\newline%
    7.52 -\verb|instance Semigroup Nat where {|\newline%
    7.53 -\verb|  mult = mult_nat;|\newline%
    7.54 -\verb|};|\newline%
    7.55 -\newline%
    7.56 -\verb|instance Monoid Nat where {|\newline%
    7.57 -\verb|  neutral = neutral_nat;|\newline%
    7.58 -\verb|};|\newline%
    7.59 -\newline%
    7.60 -\verb|bexp :: Nat -> Nat;|\newline%
    7.61 -\verb|bexp n = pow n (Suc (Suc Zero_nat));|\newline%
    7.62 -\newline%
    7.63 -\verb|}|%
    7.64 +\hspace*{0pt}module Example where {\char123}\\
    7.65 +\hspace*{0pt}\\
    7.66 +\hspace*{0pt}\\
    7.67 +\hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
    7.68 +\hspace*{0pt}\\
    7.69 +\hspace*{0pt}class Semigroup a where {\char123}\\
    7.70 +\hspace*{0pt} ~mult ::~a -> a -> a;\\
    7.71 +\hspace*{0pt}{\char125};\\
    7.72 +\hspace*{0pt}\\
    7.73 +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
    7.74 +\hspace*{0pt} ~neutral ::~a;\\
    7.75 +\hspace*{0pt}{\char125};\\
    7.76 +\hspace*{0pt}\\
    7.77 +\hspace*{0pt}pow ::~forall a. (Monoid a) => Nat -> a -> a;\\
    7.78 +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
    7.79 +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
    7.80 +\hspace*{0pt}\\
    7.81 +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
    7.82 +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
    7.83 +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
    7.84 +\hspace*{0pt}\\
    7.85 +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
    7.86 +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
    7.87 +\hspace*{0pt}\\
    7.88 +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
    7.89 +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
    7.90 +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
    7.91 +\hspace*{0pt}\\
    7.92 +\hspace*{0pt}instance Semigroup Nat where {\char123}\\
    7.93 +\hspace*{0pt} ~mult = mult{\char95}nat;\\
    7.94 +\hspace*{0pt}{\char125};\\
    7.95 +\hspace*{0pt}\\
    7.96 +\hspace*{0pt}instance Monoid Nat where {\char123}\\
    7.97 +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
    7.98 +\hspace*{0pt}{\char125};\\
    7.99 +\hspace*{0pt}\\
   7.100 +\hspace*{0pt}bexp ::~Nat -> Nat;\\
   7.101 +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
   7.102 +\hspace*{0pt}\\
   7.103 +\hspace*{0pt}{\char125}%
   7.104  \end{isamarkuptext}%
   7.105  \isamarkuptrue%
   7.106  %
   7.107 @@ -338,38 +338,38 @@
   7.108  \begin{isamarkuptext}%
   7.109  \isaverbatim%
   7.110  \noindent%
   7.111 -\verb|structure Example = |\newline%
   7.112 -\verb|struct|\newline%
   7.113 -\newline%
   7.114 -\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
   7.115 -\newline%
   7.116 -\verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline%
   7.117 -\verb|fun mult (A_:'a semigroup) = #mult A_;|\newline%
   7.118 -\newline%
   7.119 -\verb|type 'a monoid = {Program__semigroup_monoid : 'a semigroup, neutral : 'a};|\newline%
   7.120 -\verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline%
   7.121 -\verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline%
   7.122 -\newline%
   7.123 -\verb|fun pow A_ Zero_nat a = neutral A_|\newline%
   7.124 -\verb|  |\verb,|,\verb| pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a);|\newline%
   7.125 -\newline%
   7.126 -\verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline%
   7.127 -\verb|  |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
   7.128 -\newline%
   7.129 -\verb|val neutral_nat : nat = Suc Zero_nat;|\newline%
   7.130 -\newline%
   7.131 -\verb|fun mult_nat Zero_nat n = Zero_nat|\newline%
   7.132 -\verb|  |\verb,|,\verb| mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
   7.133 -\newline%
   7.134 -\verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline%
   7.135 -\newline%
   7.136 -\verb|val monoid_nat =|\newline%
   7.137 -\verb|  {Program__semigroup_monoid = semigroup_nat, neutral = neutral_nat} :|\newline%
   7.138 -\verb|  nat monoid;|\newline%
   7.139 -\newline%
   7.140 -\verb|fun bexp n = pow monoid_nat n (Suc (Suc Zero_nat));|\newline%
   7.141 -\newline%
   7.142 -\verb|end; (*struct Example*)|%
   7.143 +\hspace*{0pt}structure Example = \\
   7.144 +\hspace*{0pt}struct\\
   7.145 +\hspace*{0pt}\\
   7.146 +\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
   7.147 +\hspace*{0pt}\\
   7.148 +\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
   7.149 +\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
   7.150 +\hspace*{0pt}\\
   7.151 +\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup, neutral :~'a{\char125};\\
   7.152 +\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\
   7.153 +\hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\
   7.154 +\hspace*{0pt}\\
   7.155 +\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
   7.156 +\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
   7.157 +\hspace*{0pt}\\
   7.158 +\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
   7.159 +\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
   7.160 +\hspace*{0pt}\\
   7.161 +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
   7.162 +\hspace*{0pt}\\
   7.163 +\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
   7.164 +\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
   7.165 +\hspace*{0pt}\\
   7.166 +\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
   7.167 +\hspace*{0pt}\\
   7.168 +\hspace*{0pt}val monoid{\char95}nat =\\
   7.169 +\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat, neutral = neutral{\char95}nat{\char125}~:\\
   7.170 +\hspace*{0pt} ~nat monoid;\\
   7.171 +\hspace*{0pt}\\
   7.172 +\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
   7.173 +\hspace*{0pt}\\
   7.174 +\hspace*{0pt}end; (*struct Example*)%
   7.175  \end{isamarkuptext}%
   7.176  \isamarkuptrue%
   7.177  %
   7.178 @@ -659,23 +659,23 @@
   7.179  \begin{isamarkuptext}%
   7.180  \isaverbatim%
   7.181  \noindent%
   7.182 -\verb|structure Example = |\newline%
   7.183 -\verb|struct|\newline%
   7.184 -\newline%
   7.185 -\verb|datatype nat = Dig1 of nat |\verb,|,\verb| Dig0 of nat |\verb,|,\verb| One_nat |\verb,|,\verb| Zero_nat;|\newline%
   7.186 -\newline%
   7.187 -\verb|fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat)|\newline%
   7.188 -\verb|  |\verb,|,\verb| plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n)|\newline%
   7.189 -\verb|  |\verb,|,\verb| plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n)|\newline%
   7.190 -\verb|  |\verb,|,\verb| plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n)|\newline%
   7.191 -\verb|  |\verb,|,\verb| plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat)|\newline%
   7.192 -\verb|  |\verb,|,\verb| plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat)|\newline%
   7.193 -\verb|  |\verb,|,\verb| plus_nat (Dig0 m) One_nat = Dig1 m|\newline%
   7.194 -\verb|  |\verb,|,\verb| plus_nat One_nat (Dig0 n) = Dig1 n|\newline%
   7.195 -\verb|  |\verb,|,\verb| plus_nat m Zero_nat = m|\newline%
   7.196 -\verb|  |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
   7.197 -\newline%
   7.198 -\verb|end; (*struct Example*)|%
   7.199 +\hspace*{0pt}structure Example = \\
   7.200 +\hspace*{0pt}struct\\
   7.201 +\hspace*{0pt}\\
   7.202 +\hspace*{0pt}datatype nat = Dig1 of nat | Dig0 of nat | One{\char95}nat | Zero{\char95}nat;\\
   7.203 +\hspace*{0pt}\\
   7.204 +\hspace*{0pt}fun plus{\char95}nat (Dig1 m) (Dig1 n) = Dig0 (plus{\char95}nat (plus{\char95}nat m n) One{\char95}nat)\\
   7.205 +\hspace*{0pt} ~| plus{\char95}nat (Dig1 m) (Dig0 n) = Dig1 (plus{\char95}nat m n)\\
   7.206 +\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig1 n) = Dig1 (plus{\char95}nat m n)\\
   7.207 +\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig0 n) = Dig0 (plus{\char95}nat m n)\\
   7.208 +\hspace*{0pt} ~| plus{\char95}nat (Dig1 m) One{\char95}nat = Dig0 (plus{\char95}nat m One{\char95}nat)\\
   7.209 +\hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig1 n) = Dig0 (plus{\char95}nat n One{\char95}nat)\\
   7.210 +\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) One{\char95}nat = Dig1 m\\
   7.211 +\hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig0 n) = Dig1 n\\
   7.212 +\hspace*{0pt} ~| plus{\char95}nat m Zero{\char95}nat = m\\
   7.213 +\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
   7.214 +\hspace*{0pt}\\
   7.215 +\hspace*{0pt}end; (*struct Example*)%
   7.216  \end{isamarkuptext}%
   7.217  \isamarkuptrue%
   7.218  %
   7.219 @@ -776,25 +776,25 @@
   7.220  \begin{isamarkuptext}%
   7.221  \isaverbatim%
   7.222  \noindent%
   7.223 -\verb|structure Example = |\newline%
   7.224 -\verb|struct|\newline%
   7.225 -\newline%
   7.226 -\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
   7.227 -\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
   7.228 -\newline%
   7.229 -\verb|fun eqop A_ a b = eq A_ a b;|\newline%
   7.230 -\newline%
   7.231 -\verb|fun member A_ x [] = false|\newline%
   7.232 -\verb|  |\verb,|,\verb| member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys;|\newline%
   7.233 -\newline%
   7.234 -\verb|fun collect_duplicates A_ xs ys [] = xs|\newline%
   7.235 -\verb|  |\verb,|,\verb| collect_duplicates A_ xs ys (z :: zs) =|\newline%
   7.236 -\verb|    (if member A_ z xs|\newline%
   7.237 -\verb|      then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
   7.238 -\verb|             else collect_duplicates A_ xs (z :: ys) zs)|\newline%
   7.239 -\verb|      else collect_duplicates A_ (z :: xs) (z :: ys) zs);|\newline%
   7.240 -\newline%
   7.241 -\verb|end; (*struct Example*)|%
   7.242 +\hspace*{0pt}structure Example = \\
   7.243 +\hspace*{0pt}struct\\
   7.244 +\hspace*{0pt}\\
   7.245 +\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
   7.246 +\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
   7.247 +\hspace*{0pt}\\
   7.248 +\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
   7.249 +\hspace*{0pt}\\
   7.250 +\hspace*{0pt}fun member A{\char95}~x [] = false\\
   7.251 +\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqop A{\char95}~x y orelse member A{\char95}~x ys;\\
   7.252 +\hspace*{0pt}\\
   7.253 +\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
   7.254 +\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
   7.255 +\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
   7.256 +\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
   7.257 +\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
   7.258 +\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
   7.259 +\hspace*{0pt}\\
   7.260 +\hspace*{0pt}end; (*struct Example*)%
   7.261  \end{isamarkuptext}%
   7.262  \isamarkuptrue%
   7.263  %
   7.264 @@ -912,34 +912,34 @@
   7.265  \begin{isamarkuptext}%
   7.266  \isaverbatim%
   7.267  \noindent%
   7.268 -\verb|structure Example = |\newline%
   7.269 -\verb|struct|\newline%
   7.270 -\newline%
   7.271 -\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
   7.272 -\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
   7.273 -\newline%
   7.274 -\verb|type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};|\newline%
   7.275 -\verb|fun less_eq (A_:'a ord) = #less_eq A_;|\newline%
   7.276 -\verb|fun less (A_:'a ord) = #less A_;|\newline%
   7.277 -\newline%
   7.278 -\verb|fun eqop A_ a b = eq A_ a b;|\newline%
   7.279 -\newline%
   7.280 -\verb|type 'a preorder = {Orderings__ord_preorder : 'a ord};|\newline%
   7.281 -\verb|fun ord_preorder (A_:'a preorder) = #Orderings__ord_preorder A_;|\newline%
   7.282 -\newline%
   7.283 -\verb|type 'a order = {Orderings__preorder_order : 'a preorder};|\newline%
   7.284 -\verb|fun preorder_order (A_:'a order) = #Orderings__preorder_order A_;|\newline%
   7.285 -\newline%
   7.286 -\verb|fun less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline%
   7.287 -\verb|  less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline%
   7.288 -\verb|    eqop A1_ x1 x2 andalso|\newline%
   7.289 -\verb|      less_eq ((ord_preorder o preorder_order) B_) y1 y2|\newline%
   7.290 -\verb|  |\verb,|,\verb| less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline%
   7.291 -\verb|    less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline%
   7.292 -\verb|      eqop A1_ x1 x2 andalso|\newline%
   7.293 -\verb|        less_eq ((ord_preorder o preorder_order) B_) y1 y2;|\newline%
   7.294 -\newline%
   7.295 -\verb|end; (*struct Example*)|%
   7.296 +\hspace*{0pt}structure Example = \\
   7.297 +\hspace*{0pt}struct\\
   7.298 +\hspace*{0pt}\\
   7.299 +\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
   7.300 +\hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
   7.301 +\hspace*{0pt}\\
   7.302 +\hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool, less :~'a -> 'a -> bool{\char125};\\
   7.303 +\hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\
   7.304 +\hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\
   7.305 +\hspace*{0pt}\\
   7.306 +\hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
   7.307 +\hspace*{0pt}\\
   7.308 +\hspace*{0pt}type 'a preorder = {\char123}Orderings{\char95}{\char95}ord{\char95}preorder :~'a ord{\char125};\\
   7.309 +\hspace*{0pt}fun ord{\char95}preorder (A{\char95}:'a preorder) = {\char35}Orderings{\char95}{\char95}ord{\char95}preorder A{\char95};\\
   7.310 +\hspace*{0pt}\\
   7.311 +\hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\
   7.312 +\hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\
   7.313 +\hspace*{0pt}\\
   7.314 +\hspace*{0pt}fun less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\
   7.315 +\hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
   7.316 +\hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\
   7.317 +\hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\
   7.318 +\hspace*{0pt} ~| less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\
   7.319 +\hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
   7.320 +\hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\
   7.321 +\hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\
   7.322 +\hspace*{0pt}\\
   7.323 +\hspace*{0pt}end; (*struct Example*)%
   7.324  \end{isamarkuptext}%
   7.325  \isamarkuptrue%
   7.326  %
   7.327 @@ -1033,29 +1033,29 @@
   7.328  \begin{isamarkuptext}%
   7.329  \isaverbatim%
   7.330  \noindent%
   7.331 -\verb|structure Example = |\newline%
   7.332 -\verb|struct|\newline%
   7.333 -\newline%
   7.334 -\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
   7.335 -\newline%
   7.336 -\verb|fun null [] = true|\newline%
   7.337 -\verb|  |\verb,|,\verb| null (x :: xs) = false;|\newline%
   7.338 -\newline%
   7.339 -\verb|fun eq_nat (Suc a) Zero_nat = false|\newline%
   7.340 -\verb|  |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline%
   7.341 -\verb|  |\verb,|,\verb| eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'|\newline%
   7.342 -\verb|  |\verb,|,\verb| eq_nat Zero_nat Zero_nat = true;|\newline%
   7.343 -\newline%
   7.344 -\verb|datatype monotype = Mono of nat * monotype list;|\newline%
   7.345 -\newline%
   7.346 -\verb|fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys|\newline%
   7.347 -\verb|  |\verb,|,\verb| list_all2 p xs [] = null xs|\newline%
   7.348 -\verb|  |\verb,|,\verb| list_all2 p [] ys = null ys;|\newline%
   7.349 -\newline%
   7.350 -\verb|fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =|\newline%
   7.351 -\verb|  eq_nat tyco1 tyco2 andalso list_all2 eq_monotype typargs1 typargs2;|\newline%
   7.352 -\newline%
   7.353 -\verb|end; (*struct Example*)|%
   7.354 +\hspace*{0pt}structure Example = \\
   7.355 +\hspace*{0pt}struct\\
   7.356 +\hspace*{0pt}\\
   7.357 +\hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
   7.358 +\hspace*{0pt}\\
   7.359 +\hspace*{0pt}fun null [] = true\\
   7.360 +\hspace*{0pt} ~| null (x ::~xs) = false;\\
   7.361 +\hspace*{0pt}\\
   7.362 +\hspace*{0pt}fun eq{\char95}nat (Suc a) Zero{\char95}nat = false\\
   7.363 +\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc a) = false\\
   7.364 +\hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\
   7.365 +\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\
   7.366 +\hspace*{0pt}\\
   7.367 +\hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\
   7.368 +\hspace*{0pt}\\
   7.369 +\hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\
   7.370 +\hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\
   7.371 +\hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\
   7.372 +\hspace*{0pt}\\
   7.373 +\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =\\
   7.374 +\hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\
   7.375 +\hspace*{0pt}\\
   7.376 +\hspace*{0pt}end; (*struct Example*)%
   7.377  \end{isamarkuptext}%
   7.378  \isamarkuptrue%
   7.379  %
   7.380 @@ -1108,12 +1108,12 @@
   7.381  \begin{isamarkuptext}%
   7.382  \isaverbatim%
   7.383  \noindent%
   7.384 -\verb|strict_dequeue :: forall a. Queue a -> (a, Queue a);|\newline%
   7.385 -\verb|strict_dequeue (Queue xs (y : ys)) = (y, Queue xs ys);|\newline%
   7.386 -\verb|strict_dequeue (Queue xs []) =|\newline%
   7.387 -\verb|  let {|\newline%
   7.388 -\verb|    (y : ys) = rev xs;|\newline%
   7.389 -\verb|  } in (y, Queue [] ys);|%
   7.390 +\hspace*{0pt}strict{\char95}dequeue ::~forall a. Queue a -> (a, Queue a);\\
   7.391 +\hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y, Queue xs ys);\\
   7.392 +\hspace*{0pt}strict{\char95}dequeue (Queue xs []) =\\
   7.393 +\hspace*{0pt} ~let {\char123}\\
   7.394 +\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
   7.395 +\hspace*{0pt} ~{\char125}~in (y, Queue [] ys);%
   7.396  \end{isamarkuptext}%
   7.397  \isamarkuptrue%
   7.398  %
   7.399 @@ -1204,13 +1204,13 @@
   7.400  \begin{isamarkuptext}%
   7.401  \isaverbatim%
   7.402  \noindent%
   7.403 -\verb|empty_queue :: forall a. a;|\newline%
   7.404 -\verb|empty_queue = error "empty_queue";|\newline%
   7.405 -\newline%
   7.406 -\verb|strict_dequeue' :: forall a. Queue a -> (a, Queue a);|\newline%
   7.407 -\verb|strict_dequeue' (Queue xs []) =|\newline%
   7.408 -\verb|  (if nulla xs then empty_queue else strict_dequeue' (Queue [] (rev xs)));|\newline%
   7.409 -\verb|strict_dequeue' (Queue xs (y : ys)) = (y, Queue xs ys);|%
   7.410 +\hspace*{0pt}empty{\char95}queue ::~forall a. a;\\
   7.411 +\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
   7.412 +\hspace*{0pt}\\
   7.413 +\hspace*{0pt}strict{\char95}dequeue' ::~forall a. Queue a -> (a, Queue a);\\
   7.414 +\hspace*{0pt}strict{\char95}dequeue' (Queue xs []) =\\
   7.415 +\hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue' (Queue [] (rev xs)));\\
   7.416 +\hspace*{0pt}strict{\char95}dequeue' (Queue xs (y :~ys)) = (y, Queue xs ys);%
   7.417  \end{isamarkuptext}%
   7.418  \isamarkuptrue%
   7.419  %
     8.1 --- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Fri Oct 31 10:39:04 2008 +0100
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Nov 03 14:15:25 2008 +0100
     8.3 @@ -26,7 +26,7 @@
     8.4  \newcommand{\qt}[1]{``{#1}''}
     8.5  
     8.6  % verbatim text
     8.7 -\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
     8.8 +\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
     8.9  
    8.10  % invisibility
    8.11  \isadroptag{theory}
     9.1 --- a/doc-src/more_antiquote.ML	Fri Oct 31 10:39:04 2008 +0100
     9.2 +++ b/doc-src/more_antiquote.ML	Mon Nov 03 14:15:25 2008 +0100
     9.3 @@ -7,7 +7,7 @@
     9.4  
     9.5  signature MORE_ANTIQUOTE =
     9.6  sig
     9.7 -  val verbatim_lines: string list -> string
     9.8 +  val verbatim: string -> string
     9.9  end;
    9.10  
    9.11  structure More_Antiquote : MORE_ANTIQUOTE =
    9.12 @@ -17,12 +17,34 @@
    9.13  
    9.14  (* printing verbatim lines *)
    9.15  
    9.16 -val verbatim_line = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
    9.17 -val verbatim_lines = rev
    9.18 -  #> dropwhile (fn s => s = "")
    9.19 -  #> rev
    9.20 -  #> map verbatim_line #> space_implode "\\newline%\n"
    9.21 -  #> prefix "\\isaverbatim%\n\\noindent%\n"
    9.22 +fun verbatim s =
    9.23 +  let
    9.24 +    val parse = Scan.repeat
    9.25 +      (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
    9.26 +        || (Scan.this_string " " 
    9.27 +          || Scan.this_string ":"
    9.28 +          || Scan.this_string "\"" |-- Scan.succeed "{\\char34}"
    9.29 +          || Scan.this_string "#" |-- Scan.succeed "{\\char35}"
    9.30 +          || Scan.this_string "$" |-- Scan.succeed "{\\char36}"
    9.31 +          || Scan.this_string "%" |-- Scan.succeed "{\\char37}"
    9.32 +          || Scan.this_string "&" |-- Scan.succeed "{\\char38}"
    9.33 +          || Scan.this_string "\\" |-- Scan.succeed "{\\char92}"
    9.34 +          || Scan.this_string "^" |-- Scan.succeed "{\\char94}"
    9.35 +          || Scan.this_string "_" |-- Scan.succeed "{\\char95}"
    9.36 +          || Scan.this_string "{" |-- Scan.succeed "{\\char123}"
    9.37 +          || Scan.this_string "}" |-- Scan.succeed "{\\char125}"
    9.38 +          || Scan.this_string "~" |-- Scan.succeed "{\\char126}")
    9.39 +          -- Scan.repeat (Scan.this_string " ")
    9.40 +          >> (fn (x, xs) => x ^ replicate_string (length xs) "~")
    9.41 +        || Scan.one Symbol.not_eof);
    9.42 +    fun is_newline s = (s = "\n");
    9.43 +    val cs = explode s |> take_prefix is_newline |> snd
    9.44 +      |> take_suffix is_newline |> fst;
    9.45 +    val (texts, []) =  Scan.finite Symbol.stopper parse cs
    9.46 +  in if null texts
    9.47 +    then ""
    9.48 +    else implode ("\\isaverbatim%\n\\noindent%\n\\hspace*{0pt}" :: texts)
    9.49 +  end
    9.50  
    9.51  
    9.52  (* class antiquotation *)
    9.53 @@ -69,8 +91,7 @@
    9.54      Code_Target.code_of (ProofContext.theory_of ctxt)
    9.55        target "Example" (mk_cs (ProofContext.theory_of ctxt))
    9.56          (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
    9.57 -    |> split_lines
    9.58 -    |> verbatim_lines;
    9.59 +    |> verbatim;
    9.60  
    9.61  in
    9.62