changeset 49834 | b27bbb021df1 |
parent 48431 | 6efff142bb54 |
child 49962 | a8cc904a6820 |
--- a/src/HOL/Code_Numeral.thy Fri Oct 12 15:08:29 2012 +0200 +++ b/src/HOL/Code_Numeral.thy Fri Oct 12 18:58:20 2012 +0200 @@ -13,7 +13,7 @@ subsection {* Datatype of target language numerals *} -typedef (open) code_numeral = "UNIV \<Colon> nat set" +typedef code_numeral = "UNIV \<Colon> nat set" morphisms nat_of of_nat .. lemma of_nat_nat_of [simp]: