src/HOL/Datatype.thy
changeset 20588 c847c56edf0c
parent 20523 36a59e5d0039
child 20798 3275b03e2fff
     1.1 --- a/src/HOL/Datatype.thy	Tue Sep 19 15:21:41 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Tue Sep 19 15:21:42 2006 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  imports Datatype_Universe
     1.5  begin
     1.6  
     1.7 +setup "DatatypeCodegen.setup2"
     1.8 +
     1.9  subsection {* Representing primitive types *}
    1.10  
    1.11  rep_datatype bool
    1.12 @@ -297,4 +299,10 @@
    1.13    (SML target_atom "NONE" and target_atom "SOME")
    1.14    (Haskell target_atom "Nothing" and target_atom "Just")
    1.15  
    1.16 +code_instance option :: eq
    1.17 +  (Haskell -)
    1.18 +
    1.19 +code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
    1.20 +  (Haskell infixl 4 "==")
    1.21 +
    1.22  end