changeset 28346 | b8390cd56b8f |
parent 28228 | 7ebe8dc06cbb |
child 28562 | 4e74209f113e |
1.1 --- a/src/HOL/Library/Code_Integer.thy Wed Sep 24 19:39:25 2008 +0200 1.2 +++ b/src/HOL/Library/Code_Integer.thy Thu Sep 25 09:28:03 2008 +0200 1.3 @@ -72,7 +72,7 @@ 1.4 (OCaml "Big'_int.mult'_big'_int") 1.5 (Haskell infixl 7 "*") 1.6 1.7 -code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool" 1.8 +code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool" 1.9 (SML "!((_ : IntInf.int) = _)") 1.10 (OCaml "Big'_int.eq'_big'_int") 1.11 (Haskell infixl 4 "==")