changeset 38763 | 283f1f9969ba |
parent 38715 | 6513ea67d95d |
child 38864 | 4abe644fcea5 |
--- a/src/HOL/Tools/int_arith.ML Thu Aug 26 17:37:26 2010 +0200 +++ b/src/HOL/Tools/int_arith.ML Thu Aug 26 20:42:09 2010 +0200 @@ -91,7 +91,7 @@ fun number_of thy T n = if not (Sign.of_sort thy (T, @{sort number})) then raise CTERM ("number_of", []) - else Numeral.mk_cnumber (Thm.ctyp_of thy T) n + else Numeral.mk_cnumber (Thm.ctyp_of thy T) n; val setup = Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]