src/HOL/Code_Numeral.thy
changeset 55414 eab03e9cee8a
parent 54489 03ff4d1e6784
child 55416 dd7992d4a61a
     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -375,7 +375,7 @@
     1.4      by (auto simp add: sgn_if)
     1.5    have aux2: "\<And>q::int. - int_of_integer k = int_of_integer l * q \<longleftrightarrow> int_of_integer k = int_of_integer l * - q" by auto
     1.6    show ?thesis
     1.7 -    by (simp add: prod_eq_iff integer_eq_iff prod_case_beta aux1)
     1.8 +    by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1)
     1.9        (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
    1.10  qed
    1.11  
    1.12 @@ -466,7 +466,7 @@
    1.13    }
    1.14    note aux = this
    1.15    show ?thesis
    1.16 -    by (auto simp add: num_of_integer_def nat_of_integer_def Let_def prod_case_beta
    1.17 +    by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta
    1.18        not_le integer_eq_iff less_eq_integer_def
    1.19        nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
    1.20         mult_2 [where 'a=nat] aux add_One)