equal
deleted
inserted
replaced
12 *} |
12 *} |
13 |
13 |
14 subsection {* Datatype of target language numerals *} |
14 subsection {* Datatype of target language numerals *} |
15 |
15 |
16 typedef (open) code_numeral = "UNIV \<Colon> nat set" |
16 typedef (open) code_numeral = "UNIV \<Colon> nat set" |
17 morphisms nat_of of_nat by rule |
17 morphisms nat_of of_nat .. |
18 |
18 |
19 lemma of_nat_nat_of [simp]: |
19 lemma of_nat_nat_of [simp]: |
20 "of_nat (nat_of k) = k" |
20 "of_nat (nat_of k) = k" |
21 by (rule nat_of_inverse) |
21 by (rule nat_of_inverse) |
22 |
22 |