doc-src/Codegen/Thy/Adaptation.thy

 
 subsection {* @{text Haskell} serialisation *}
 
 text {*
   For convenience, the default @{text HOL} setup for @{text Haskell}
-  maps the @{class eq} class to its counterpart in @{text Haskell},
-  giving custom serialisations for the class @{class eq} (by command
-  @{command_def code_class}) and its operation @{const HOL.eq}
-*}
-
-code_class %quotett eq
+  maps the @{class equal} class to its counterpart in @{text Haskell},
+  giving custom serialisations for the class @{class equal} (by command
+  @{command_def code_class}) and its operation @{const HOL.equal}
+*}
+
+code_class %quotett equal
   (Haskell "Eq")
 
 code_const %quotett "op ="
   (Haskell infixl 4 "==")
 
 text {*
   \noindent A problem now occurs whenever a type which is an instance
-  of @{class eq} in @{text HOL} is mapped on a @{text
+  of @{class equal} in @{text HOL} is mapped on a @{text
   Haskell}-built-in type which is also an instance of @{text Haskell}
   @{text Eq}:
 *}
 
 typedecl %quote bar
 
-instantiation %quote bar :: eq
+instantiation %quote bar :: equal
 begin
 
-definition %quote "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
-
-instance %quote by default (simp add: eq_bar_def)
+definition %quote "HOL.equal (x\<Colon>bar) y \<longleftrightarrow> x = y"
+
+instance %quote by default (simp add: equal_bar_def)
 
 end %quote (*<*)
 
 (*>*) code_type %quotett bar
   (Haskell "Integer")

   \noindent The code generator would produce an additional instance,
   which of course is rejected by the @{text Haskell} compiler.  To
   suppress this additional instance, use @{command_def "code_instance"}:
 *}
 
-code_instance %quotett bar :: eq
+code_instance %quotett bar :: equal
   (Haskell -)
 
 
 subsection {* Enhancing the target language context \label{sec:include} *}