1.1 --- a/src/HOL/Code_Numeral.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -115,12 +115,12 @@
     1.4  lemmas [code del] = code_numeral.recs code_numeral.cases
     1.5  
     1.6  lemma [code]:
     1.7 -  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
     1.8 -  by (cases k, cases l) (simp add: eq)
     1.9 +  "HOL.equal k l \<longleftrightarrow> HOL.equal (nat_of k) (nat_of l)"
    1.10 +  by (cases k, cases l) (simp add: equal)
    1.11  
    1.12  lemma [code nbe]:
    1.13 -  "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
    1.14 -  by (rule HOL.eq_refl)
    1.15 +  "HOL.equal (k::code_numeral) k \<longleftrightarrow> True"
    1.16 +  by (rule equal_refl)
    1.17  
    1.18  
    1.19  subsection {* Code numerals as datatype of ints *}
    1.20 @@ -301,7 +301,7 @@
    1.21    (Haskell "Integer")
    1.22    (Scala "BigInt")
    1.23  
    1.24 -code_instance code_numeral :: eq
    1.25 +code_instance code_numeral :: equal
    1.26    (Haskell -)
    1.27  
    1.28  setup {*
    1.29 @@ -342,7 +342,7 @@
    1.30    (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
    1.31    (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.32  
    1.33 -code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.34 +code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.35    (SML "!((_ : Int.int) = _)")
    1.36    (OCaml "Big'_int.eq'_big'_int")
    1.37    (Haskell infixl 4 "==")