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