src/HOL/Library/Code_Natural.thy
changeset 38857 97775f3e8722
parent 38810 361119ea62ee
child 38968 e55deaa22fff
     1.1 --- a/src/HOL/Library/Code_Natural.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Natural.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4      false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
     1.5  *}
     1.6  
     1.7 -code_instance code_numeral :: eq
     1.8 +code_instance code_numeral :: equal
     1.9    (Haskell -)
    1.10  
    1.11  code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.12 @@ -131,7 +131,7 @@
    1.13    (Haskell "divMod")
    1.14    (Scala infixl 8 "/%")
    1.15  
    1.16 -code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.17 +code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.18    (Haskell infixl 4 "==")
    1.19    (Scala infixl 5 "==")
    1.20