src/HOL/Code_Numeral.thy
changeset 59487 adaa430fc0f7
parent 58889 5b7a9633cfa8
child 59816 034b13f4efae
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Feb 06 19:17:17 2015 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Feb 06 17:57:03 2015 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  typedef integer = "UNIV \<Colon> int set"
     1.5    morphisms int_of_integer integer_of_int ..
     1.6  
     1.7 -setup_lifting (no_code) type_definition_integer
     1.8 +setup_lifting type_definition_integer
     1.9  
    1.10  lemma integer_eq_iff:
    1.11    "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
    1.12 @@ -620,7 +620,7 @@
    1.13  typedef natural = "UNIV \<Colon> nat set"
    1.14    morphisms nat_of_natural natural_of_nat ..
    1.15  
    1.16 -setup_lifting (no_code) type_definition_natural
    1.17 +setup_lifting type_definition_natural
    1.18  
    1.19  lemma natural_eq_iff [termination_simp]:
    1.20    "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"