| changeset 28346 | b8390cd56b8f |
| parent 28228 | 7ebe8dc06cbb |
| child 28351 | abfc66969d1f |
--- a/src/HOL/Library/Efficient_Nat.thy Wed Sep 24 19:39:25 2008 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Thu Sep 25 09:28:03 2008 +0200 @@ -400,7 +400,7 @@ (OCaml "Big'_int.quomod'_big'_int") (Haskell "divMod") -code_const "op = \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" +code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" (SML "!((_ : IntInf.int) = _)") (OCaml "Big'_int.eq'_big'_int") (Haskell infixl 4 "==")