updated
authorhaftmann
Tue Sep 18 10:44:02 2007 +0200 (2007-09-18)
changeset 2462833137422d7fd
parent 24627 cc6768509ed3
child 24629 65947eb930fa
updated
doc-src/IsarAdvanced/Classes/Thy/Classes.thy
doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs
doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML
doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml
doc-src/manual.bib
     1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Sep 18 08:28:47 2007 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Sep 18 10:44:02 2007 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  (* $Id$ *)
     1.6  
     1.7  (*<*)
     1.8 @@ -7,7 +6,7 @@
     1.9  begin
    1.10  
    1.11  ML {*
    1.12 -CodegenSerializer.code_width := 74;
    1.13 +CodeTarget.code_width := 74;
    1.14  *}
    1.15  
    1.16  syntax
    1.17 @@ -189,7 +188,7 @@
    1.18  *}
    1.19  
    1.20      instance int :: semigroup
    1.21 -      mult_int_def: "\<And>i j \<Colon> int. i \<otimes> j \<equiv> i + j"
    1.22 +      mult_int_def: "i \<otimes> j \<equiv> i + j"
    1.23      proof
    1.24        fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
    1.25        then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" unfolding mult_int_def .
    1.26 @@ -504,7 +503,7 @@
    1.27    \noindent This maps to Haskell as:
    1.28  *}
    1.29  
    1.30 -export_code example in Haskell to Classes file "code_examples/"
    1.31 +export_code example in Haskell module_name Classes file "code_examples/"
    1.32    (* NOTE: you may use Haskell only once in this document, otherwise
    1.33    you have to work in distinct subdirectories *)
    1.34  
    1.35 @@ -514,7 +513,7 @@
    1.36    \noindent The whole code in SML with explicit dictionary passing:
    1.37  *}
    1.38  
    1.39 -export_code example (*<*)in SML to Classes(*>*)in SML to Classes file "code_examples/classes.ML"
    1.40 +export_code example (*<*)in SML module_name Classes(*>*)in SML module_name Classes file "code_examples/classes.ML"
    1.41  
    1.42  text {*
    1.43    \lstsml{Thy/code_examples/classes.ML}
     2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Tue Sep 18 08:28:47 2007 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Tue Sep 18 10:44:02 2007 +0200
     2.3 @@ -1,25 +1,26 @@
     2.4  module Classes where {
     2.5  
     2.6  
     2.7 -data Nat = Zero_nat | Suc Nat;
     2.8 +data Nat = Suc Classes.Nat | Zero_nat;
     2.9  
    2.10 -data Bit = B0 | B1;
    2.11 +data Bit = B1 | B0;
    2.12  
    2.13 -nat_aux :: Integer -> Nat -> Nat;
    2.14 -nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));
    2.15 +nat_aux :: Integer -> Classes.Nat -> Classes.Nat;
    2.16 +nat_aux i n =
    2.17 +  (if i <= 0 then n else Classes.nat_aux (i - 1) (Classes.Suc n));
    2.18  
    2.19 -nat :: Integer -> Nat;
    2.20 -nat i = nat_aux i Zero_nat;
    2.21 +nat :: Integer -> Classes.Nat;
    2.22 +nat i = Classes.nat_aux i Classes.Zero_nat;
    2.23  
    2.24  class Semigroup a where {
    2.25    mult :: a -> a -> a;
    2.26  };
    2.27  
    2.28 -class (Semigroup a) => Monoidl a where {
    2.29 +class (Classes.Semigroup a) => Monoidl a where {
    2.30    neutral :: a;
    2.31  };
    2.32  
    2.33 -class (Monoidl a) => Group a where {
    2.34 +class (Classes.Monoidl a) => Group a where {
    2.35    inverse :: a -> a;
    2.36  };
    2.37  
    2.38 @@ -32,28 +33,28 @@
    2.39  mult_int :: Integer -> Integer -> Integer;
    2.40  mult_int i j = i + j;
    2.41  
    2.42 -instance Semigroup Integer where {
    2.43 -  mult = mult_int;
    2.44 +instance Classes.Semigroup Integer where {
    2.45 +  mult = Classes.mult_int;
    2.46  };
    2.47  
    2.48 -instance Monoidl Integer where {
    2.49 -  neutral = neutral_int;
    2.50 +instance Classes.Monoidl Integer where {
    2.51 +  neutral = Classes.neutral_int;
    2.52  };
    2.53  
    2.54 -instance Group Integer where {
    2.55 -  inverse = inverse_int;
    2.56 +instance Classes.Group Integer where {
    2.57 +  inverse = Classes.inverse_int;
    2.58  };
    2.59  
    2.60 -pow_nat :: (Group b) => Nat -> b -> b;
    2.61 -pow_nat (Suc n) x = mult x (pow_nat n x);
    2.62 -pow_nat Zero_nat x = neutral;
    2.63 +pow_nat :: (Classes.Group b) => Classes.Nat -> b -> b;
    2.64 +pow_nat (Classes.Suc n) x = Classes.mult x (Classes.pow_nat n x);
    2.65 +pow_nat Classes.Zero_nat x = Classes.neutral;
    2.66  
    2.67 -pow_int :: (Group a) => Integer -> a -> a;
    2.68 +pow_int :: (Classes.Group a) => Integer -> a -> a;
    2.69  pow_int k x =
    2.70 -  (if 0 <= k then pow_nat (nat k) x
    2.71 -    else inverse (pow_nat (nat (negate k)) x));
    2.72 +  (if 0 <= k then Classes.pow_nat (Classes.nat k) x
    2.73 +    else Classes.inverse (Classes.pow_nat (Classes.nat (negate k)) x));
    2.74  
    2.75  example :: Integer;
    2.76 -example = pow_int 10 (-2);
    2.77 +example = Classes.pow_int 10 (-2);
    2.78  
    2.79  }
     3.1 --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Tue Sep 18 08:28:47 2007 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Tue Sep 18 10:44:02 2007 +0200
     3.3 @@ -1,9 +1,9 @@
     3.4  structure Classes = 
     3.5  struct
     3.6  
     3.7 -datatype nat = Zero_nat | Suc of nat;
     3.8 +datatype nat = Suc of nat | Zero_nat;
     3.9  
    3.10 -datatype bit = B0 | B1;
    3.11 +datatype bit = B1 | B0;
    3.12  
    3.13  fun nat_aux i n =
    3.14    (if IntInf.<= (i, (0 : IntInf.int)) then n
     4.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Sep 18 08:28:47 2007 +0200
     4.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Sep 18 10:44:02 2007 +0200
     4.3 @@ -4,7 +4,6 @@
     4.4  %
     4.5  \isadelimtheory
     4.6  \isanewline
     4.7 -\isanewline
     4.8  %
     4.9  \endisadelimtheory
    4.10  %
    4.11 @@ -172,7 +171,7 @@
    4.12  \isamarkuptrue%
    4.13  \ \ \ \ \isacommand{instance}\isamarkupfalse%
    4.14  \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
    4.15 -\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isasymColon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
    4.16 +\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
    4.17  %
    4.18  \isadelimproof
    4.19  \ \ \ \ %
    4.20 @@ -733,16 +732,16 @@
    4.21  \noindent This maps to Haskell as:%
    4.22  \end{isamarkuptext}%
    4.23  \isamarkuptrue%
    4.24 -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    4.25 -\ example\ \isakeyword{in}\ Haskell\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
    4.26 +\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
    4.27 +\ example\ \isakeyword{in}\ Haskell\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
    4.28  \begin{isamarkuptext}%
    4.29  \lsthaskell{Thy/code_examples/Classes.hs}
    4.30  
    4.31    \noindent The whole code in SML with explicit dictionary passing:%
    4.32  \end{isamarkuptext}%
    4.33  \isamarkuptrue%
    4.34 -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    4.35 -\ example\ \isakeyword{in}\ SML\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
    4.36 +\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
    4.37 +\ example\ \isakeyword{in}\ SML\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
    4.38  \begin{isamarkuptext}%
    4.39  \lstsml{Thy/code_examples/classes.ML}%
    4.40  \end{isamarkuptext}%
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Sep 18 08:28:47 2007 +0200
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Sep 18 10:44:02 2007 +0200
     5.3 @@ -1198,7 +1198,7 @@
     5.4    \end{description}
     5.5  *}
     5.6  
     5.7 -subsubsection {* Datatype hooks *}
     5.8 +(*subsubsection {* Datatype hooks *}
     5.9  
    5.10  text {*
    5.11    Isabelle/HOL's datatype package provides a mechanism to
    5.12 @@ -1311,7 +1311,9 @@
    5.13       the block.
    5.14  
    5.15    \end{description}
    5.16 +*}*)
    5.17  
    5.18 +text {*
    5.19    \emph{Happy proving, happy hacking!}
    5.20  *}
    5.21  
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Sep 18 08:28:47 2007 +0200
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Tue Sep 18 10:44:02 2007 +0200
     6.3 @@ -1707,171 +1707,8 @@
     6.4  \end{isamarkuptext}%
     6.5  \isamarkuptrue%
     6.6  %
     6.7 -\isamarkupsubsubsection{Datatype hooks%
     6.8 -}
     6.9 -\isamarkuptrue%
    6.10 -%
    6.11  \begin{isamarkuptext}%
    6.12 -Isabelle/HOL's datatype package provides a mechanism to
    6.13 -  extend theories depending on datatype declarations:
    6.14 -  \emph{datatype hooks}.  For example, when declaring a new
    6.15 -  datatype, a hook proves defining equations for equality on
    6.16 -  that datatype (if possible).%
    6.17 -\end{isamarkuptext}%
    6.18 -\isamarkuptrue%
    6.19 -%
    6.20 -\isadelimmlref
    6.21 -%
    6.22 -\endisadelimmlref
    6.23 -%
    6.24 -\isatagmlref
    6.25 -%
    6.26 -\begin{isamarkuptext}%
    6.27 -\begin{mldecls}
    6.28 -  \indexmltype{DatatypeHooks.hook}\verb|type DatatypeHooks.hook = string list -> theory -> theory| \\
    6.29 -  \indexml{DatatypeHooks.add}\verb|DatatypeHooks.add: DatatypeHooks.hook -> theory -> theory|
    6.30 -  \end{mldecls}
    6.31 -
    6.32 -  \begin{description}
    6.33 -
    6.34 -  \item \verb|DatatypeHooks.hook| specifies the interface
    6.35 -     of \emph{datatype hooks}: a theory update
    6.36 -     depending on the list of newly introduced
    6.37 -     datatype names.
    6.38 -
    6.39 -  \item \verb|DatatypeHooks.add| adds a hook to the
    6.40 -     chain of all hooks.
    6.41 -
    6.42 -  \end{description}%
    6.43 -\end{isamarkuptext}%
    6.44 -\isamarkuptrue%
    6.45 -%
    6.46 -\endisatagmlref
    6.47 -{\isafoldmlref}%
    6.48 -%
    6.49 -\isadelimmlref
    6.50 -%
    6.51 -\endisadelimmlref
    6.52 -%
    6.53 -\isamarkupsubsubsection{Trivial typedefs -- type copies%
    6.54 -}
    6.55 -\isamarkuptrue%
    6.56 -%
    6.57 -\begin{isamarkuptext}%
    6.58 -Sometimes packages will introduce new types
    6.59 -  as \emph{marked type copies} similar to Haskell's
    6.60 -  \isa{newtype} declaration (e.g. the HOL record package)
    6.61 -  \emph{without} tinkering with the overhead of datatypes.
    6.62 -  Technically, these type copies are trivial forms of typedefs.
    6.63 -  Since these type copies in code generation view are nothing
    6.64 -  else than datatypes, they have been given a own package
    6.65 -  in order to faciliate code generation:%
    6.66 -\end{isamarkuptext}%
    6.67 -\isamarkuptrue%
    6.68 -%
    6.69 -\isadelimmlref
    6.70 -%
    6.71 -\endisadelimmlref
    6.72 -%
    6.73 -\isatagmlref
    6.74 -%
    6.75 -\begin{isamarkuptext}%
    6.76 -\begin{mldecls}
    6.77 -  \indexmltype{TypecopyPackage.info}\verb|type TypecopyPackage.info| \\
    6.78 -  \indexml{TypecopyPackage.add-typecopy}\verb|TypecopyPackage.add_typecopy: |\isasep\isanewline%
    6.79 -\verb|    bstring * string list -> typ -> (bstring * bstring) option|\isasep\isanewline%
    6.80 -\verb|    -> theory -> (string * TypecopyPackage.info) * theory| \\
    6.81 -  \indexml{TypecopyPackage.get-typecopy-info}\verb|TypecopyPackage.get_typecopy_info: theory|\isasep\isanewline%
    6.82 -\verb|    -> string -> TypecopyPackage.info option| \\
    6.83 -  \indexml{TypecopyPackage.get-spec}\verb|TypecopyPackage.get_spec: theory -> string|\isasep\isanewline%
    6.84 -\verb|    -> (string * sort) list * (string * typ list) list| \\
    6.85 -  \indexmltype{TypecopyPackage.hook}\verb|type TypecopyPackage.hook = string * TypecopyPackage.info -> theory -> theory| \\
    6.86 -  \indexml{TypecopyPackage.add-hook}\verb|TypecopyPackage.add_hook: TypecopyPackage.hook -> theory -> theory| \\
    6.87 -  \end{mldecls}
    6.88 -
    6.89 -  \begin{description}
    6.90 -
    6.91 -  \item \verb|TypecopyPackage.info| a record containing
    6.92 -     the specification and further data of a type copy.
    6.93 -
    6.94 -  \item \verb|TypecopyPackage.add_typecopy| defines a new
    6.95 -     type copy.
    6.96 -
    6.97 -  \item \verb|TypecopyPackage.get_typecopy_info| retrieves
    6.98 -     data of an existing type copy.
    6.99 -
   6.100 -  \item \verb|TypecopyPackage.get_spec| retrieves datatype-like
   6.101 -     specification of a type copy.
   6.102 -
   6.103 -  \item \verb|TypecopyPackage.hook|,~\verb|TypecopyPackage.add_hook|
   6.104 -     provide a hook mechanism corresponding to the hook mechanism
   6.105 -     on datatypes.
   6.106 -
   6.107 -  \end{description}%
   6.108 -\end{isamarkuptext}%
   6.109 -\isamarkuptrue%
   6.110 -%
   6.111 -\endisatagmlref
   6.112 -{\isafoldmlref}%
   6.113 -%
   6.114 -\isadelimmlref
   6.115 -%
   6.116 -\endisadelimmlref
   6.117 -%
   6.118 -\isamarkupsubsubsection{Unifying type copies and datatypes%
   6.119 -}
   6.120 -\isamarkuptrue%
   6.121 -%
   6.122 -\begin{isamarkuptext}%
   6.123 -Since datatypes and type copies are mapped to the same concept (datatypes)
   6.124 -  by code generation, the view on both is unified \qt{code types}:%
   6.125 -\end{isamarkuptext}%
   6.126 -\isamarkuptrue%
   6.127 -%
   6.128 -\isadelimmlref
   6.129 -%
   6.130 -\endisadelimmlref
   6.131 -%
   6.132 -\isatagmlref
   6.133 -%
   6.134 -\begin{isamarkuptext}%
   6.135 -\begin{mldecls}
   6.136 -  \indexmltype{DatatypeCodegen.hook}\verb|type DatatypeCodegen.hook = (string * (bool * ((string * sort) list|\isasep\isanewline%
   6.137 -\verb|    * (string * typ list) list))) list|\isasep\isanewline%
   6.138 -\verb|    -> theory -> theory| \\
   6.139 -  \indexml{DatatypeCodegen.add-codetypes-hook-bootstrap}\verb|DatatypeCodegen.add_codetypes_hook_bootstrap: |\isasep\isanewline%
   6.140 -\verb|      DatatypeCodegen.hook -> theory -> theory|
   6.141 -  \end{mldecls}%
   6.142 -\end{isamarkuptext}%
   6.143 -\isamarkuptrue%
   6.144 -%
   6.145 -\endisatagmlref
   6.146 -{\isafoldmlref}%
   6.147 -%
   6.148 -\isadelimmlref
   6.149 -%
   6.150 -\endisadelimmlref
   6.151 -%
   6.152 -\begin{isamarkuptext}%
   6.153 -\begin{description}
   6.154 -
   6.155 -  \item \verb|DatatypeCodegen.hook| specifies the code type hook
   6.156 -     interface: a theory transformation depending on a list of
   6.157 -     mutual recursive code types; each entry in the list
   6.158 -     has the structure \isa{{\isacharparenleft}name{\isacharcomma}\ {\isacharparenleft}is{\isacharunderscore}data{\isacharcomma}\ {\isacharparenleft}vars{\isacharcomma}\ cons{\isacharparenright}{\isacharparenright}{\isacharparenright}}
   6.159 -     where \isa{name} is the name of the code type, \isa{is{\isacharunderscore}data}
   6.160 -     is true iff \isa{name} is a datatype rather then a type copy,
   6.161 -     and \isa{{\isacharparenleft}vars{\isacharcomma}\ cons{\isacharparenright}} is the specification of the code type.
   6.162 -
   6.163 -  \item \verb|DatatypeCodegen.add_codetypes_hook_bootstrap| adds a code
   6.164 -     type hook;  the hook is immediately processed for all already
   6.165 -     existing datatypes, in blocks of mutual recursive datatypes,
   6.166 -     where all datatypes a block depends on are processed before
   6.167 -     the block.
   6.168 -
   6.169 -  \end{description}
   6.170 -
   6.171 -  \emph{Happy proving, happy hacking!}%
   6.172 +\emph{Happy proving, happy hacking!}%
   6.173  \end{isamarkuptext}%
   6.174  \isamarkuptrue%
   6.175  %
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Tue Sep 18 08:28:47 2007 +0200
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Tue Sep 18 10:44:02 2007 +0200
     7.3 @@ -10,7 +10,7 @@
     7.4  heada (x : xs) = x;
     7.5  heada [] = Codegen.nulla;
     7.6  
     7.7 -instance Codegen.Null (Maybe b) where {
     7.8 +instance Codegen.Null (Maybe a) where {
     7.9    nulla = Nothing;
    7.10  };
    7.11  
     8.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Tue Sep 18 08:28:47 2007 +0200
     8.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Tue Sep 18 10:44:02 2007 +0200
     8.3 @@ -14,7 +14,7 @@
     8.4  fun head B_ (x :: xs) = x
     8.5    | head B_ [] = null B_;
     8.6  
     8.7 -fun null_option () = {null = NONE} : ('b option) null;
     8.8 +fun null_option () = {null = NONE} : ('a option) null;
     8.9  
    8.10  val dummy : Nat.nat option =
    8.11    head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
     9.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Tue Sep 18 08:28:47 2007 +0200
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Tue Sep 18 10:44:02 2007 +0200
     9.3 @@ -14,7 +14,7 @@
     9.4  let rec head _B = function x :: xs -> x
     9.5                    | [] -> null _B;;
     9.6  
     9.7 -let null_option () = ({null = None} : ('b option) null);;
     9.8 +let null_option () = ({null = None} : ('a option) null);;
     9.9  
    9.10  let rec dummy
    9.11    = head (null_option ()) [Some (Nat.Suc Nat.Zero_nat); None];;
    10.1 --- a/doc-src/manual.bib	Tue Sep 18 08:28:47 2007 +0200
    10.2 +++ b/doc-src/manual.bib	Tue Sep 18 10:44:02 2007 +0200
    10.3 @@ -444,15 +444,23 @@
    10.4  @InProceedings{Haftmann-Wenzel:2006:classes,
    10.5    author        = {Florian Haftmann and Makarius Wenzel},
    10.6    title         = {Constructive Type Classes in {Isabelle}},
    10.7 -  year          = 2006,
    10.8 -  note          = {To appear; \url{http://www4.in.tum.de/~haftmann/pdf/constructive_type_classes_haftmann_wenzel.pdf}}
    10.9 +  editor        = {T. Altenkirch and C. McBride},
   10.10 +  booktitle     = {Types for Proofs and Programs, TYPES 2006},
   10.11 +  publisher     = {Springer},
   10.12 +  series        = {LNCS},
   10.13 +  volume        = {4502},
   10.14 +  year          = {2007}
   10.15  }
   10.16  
   10.17  @TechReport{Haftmann-Nipkow:2007:codegen,
   10.18    author        = {Florian Haftmann and Tobias Nipkow},
   10.19    title         = {A Code Generator Framework for {Isabelle/HOL}},
   10.20 -  year          = 2007,
   10.21 -  note          = {\url{http://www4.in.tum.de/~haftmann/pdf/codegen_isabelle_haftmann_nipkow_16pp.pdf}}
   10.22 +  editor        = {Klaus Schneider and Jens Brandt},
   10.23 +  booktitle     = {Theorem Proving in Higher Order Logics: Emerging Trends Proceedings},
   10.24 +  month         = {08},
   10.25 +  year          = {2007},
   10.26 +  institution   = {Department of Computer Science, University of Kaiserslautern},
   10.27 +  number        = {364/07}
   10.28  }
   10.29  
   10.30  @manual{isabelle-classes,