src/HOL/Code_Numeral.thy
changeset 66839 909ba5ed93dd
parent 66838 17989f6bc7b2
child 66886 960509bfd47e
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Oct 09 19:10:49 2017 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Oct 09 19:10:51 2017 +0200
     1.3 @@ -263,7 +263,7 @@
     1.4    by transfer (simp add: division_segment_int_def)
     1.5  
     1.6  instance integer :: ring_parity
     1.7 -  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
     1.8 +  by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
     1.9  
    1.10  instantiation integer :: unique_euclidean_semiring_numeral
    1.11  begin
    1.12 @@ -891,7 +891,7 @@
    1.13    by (simp add: natural_eq_iff)
    1.14  
    1.15  instance natural :: semiring_parity
    1.16 -  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
    1.17 +  by (standard; transfer) simp_all
    1.18  
    1.19  lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
    1.20    is "nat :: int \<Rightarrow> nat"