changeset 49834 | b27bbb021df1 |
parent 48075 | ec5e62b868eb |
--- a/src/HOL/Library/Target_Numeral.thy Fri Oct 12 15:08:29 2012 +0200 +++ b/src/HOL/Library/Target_Numeral.thy Fri Oct 12 18:58:20 2012 +0200 @@ -4,7 +4,7 @@ subsection {* Type of target language numerals *} -typedef (open) int = "UNIV \<Colon> int set" +typedef int = "UNIV \<Colon> int set" morphisms int_of of_int .. hide_type (open) int