src/HOL/NatBin.thy
changeset 25481 aa16cd919dcc
parent 24093 5d0ecd0c8f3c
child 25571 c9e39eafc7a0
     1.1 --- a/src/HOL/NatBin.thy	Tue Nov 27 21:06:52 2007 +0100
     1.2 +++ b/src/HOL/NatBin.thy	Wed Nov 28 09:01:34 2007 +0100
     1.3 @@ -652,8 +652,7 @@
     1.4  
     1.5  ML
     1.6  {*
     1.7 -val numerals = thms"numerals";
     1.8 -val numeral_ss = simpset() addsimps numerals;
     1.9 +val numeral_ss = simpset() addsimps @{thms numerals};
    1.10  
    1.11  val nat_bin_arith_setup =
    1.12   LinArith.map_data
    1.13 @@ -662,8 +661,8 @@
    1.14        inj_thms = inj_thms,
    1.15        lessD = lessD, neqE = neqE,
    1.16        simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
    1.17 -                                  not_neg_number_of_Pls,
    1.18 -                                  neg_number_of_Min,neg_number_of_BIT]})
    1.19 +        @{thm not_neg_number_of_Pls}, @{thm neg_number_of_Min},
    1.20 +        @{thm neg_number_of_BIT}]})
    1.21  *}
    1.22  
    1.23  declaration {* K nat_bin_arith_setup *}
    1.24 @@ -834,79 +833,4 @@
    1.25       "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
    1.26  by (simp add: nat_mult_div_cancel1)
    1.27  
    1.28 -
    1.29 -subsection {* legacy ML bindings *}
    1.30 -
    1.31 -ML
    1.32 -{*
    1.33 -val eq_nat_nat_iff = thm"eq_nat_nat_iff";
    1.34 -val eq_nat_number_of = thm"eq_nat_number_of";
    1.35 -val less_nat_number_of = thm"less_nat_number_of";
    1.36 -val power2_eq_square = thm "power2_eq_square";
    1.37 -val zero_le_power2 = thm "zero_le_power2";
    1.38 -val zero_less_power2 = thm "zero_less_power2";
    1.39 -val zero_eq_power2 = thm "zero_eq_power2";
    1.40 -val abs_power2 = thm "abs_power2";
    1.41 -val power2_abs = thm "power2_abs";
    1.42 -val power2_minus = thm "power2_minus";
    1.43 -val power_minus1_even = thm "power_minus1_even";
    1.44 -val power_minus_even = thm "power_minus_even";
    1.45 -val odd_power_less_zero = thm "odd_power_less_zero";
    1.46 -val odd_0_le_power_imp_0_le = thm "odd_0_le_power_imp_0_le";
    1.47 -
    1.48 -val Suc_pred' = thm"Suc_pred'";
    1.49 -val expand_Suc = thm"expand_Suc";
    1.50 -val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1";
    1.51 -val Suc_eq_add_numeral_1_left = thm"Suc_eq_add_numeral_1_left";
    1.52 -val add_eq_if = thm"add_eq_if";
    1.53 -val mult_eq_if = thm"mult_eq_if";
    1.54 -val power_eq_if = thm"power_eq_if";
    1.55 -val eq_number_of_0 = thm"eq_number_of_0";
    1.56 -val eq_0_number_of = thm"eq_0_number_of";
    1.57 -val less_0_number_of = thm"less_0_number_of";
    1.58 -val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0";
    1.59 -val eq_number_of_Suc = thm"eq_number_of_Suc";
    1.60 -val Suc_eq_number_of = thm"Suc_eq_number_of";
    1.61 -val less_number_of_Suc = thm"less_number_of_Suc";
    1.62 -val less_Suc_number_of = thm"less_Suc_number_of";
    1.63 -val le_number_of_Suc = thm"le_number_of_Suc";
    1.64 -val le_Suc_number_of = thm"le_Suc_number_of";
    1.65 -val eq_number_of_BIT_BIT = thm"eq_number_of_BIT_BIT";
    1.66 -val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
    1.67 -val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
    1.68 -val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
    1.69 -val of_nat_number_of_eq = thm"of_nat_number_of_eq";
    1.70 -val nat_power_eq = thm"nat_power_eq";
    1.71 -val power_nat_number_of = thm"power_nat_number_of";
    1.72 -val zpower_number_of_even = thm"zpower_number_of_even";
    1.73 -val zpower_number_of_odd = thm"zpower_number_of_odd";
    1.74 -val nat_number_of_Pls = thm"nat_number_of_Pls";
    1.75 -val nat_number_of_Min = thm"nat_number_of_Min";
    1.76 -val Let_Suc = thm"Let_Suc";
    1.77 -
    1.78 -val nat_number = thms"nat_number";
    1.79 -
    1.80 -val nat_number_of_add_left = thm"nat_number_of_add_left";
    1.81 -val nat_number_of_mult_left = thm"nat_number_of_mult_left";
    1.82 -val left_add_mult_distrib = thm"left_add_mult_distrib";
    1.83 -val nat_diff_add_eq1 = thm"nat_diff_add_eq1";
    1.84 -val nat_diff_add_eq2 = thm"nat_diff_add_eq2";
    1.85 -val nat_eq_add_iff1 = thm"nat_eq_add_iff1";
    1.86 -val nat_eq_add_iff2 = thm"nat_eq_add_iff2";
    1.87 -val nat_less_add_iff1 = thm"nat_less_add_iff1";
    1.88 -val nat_less_add_iff2 = thm"nat_less_add_iff2";
    1.89 -val nat_le_add_iff1 = thm"nat_le_add_iff1";
    1.90 -val nat_le_add_iff2 = thm"nat_le_add_iff2";
    1.91 -val nat_mult_le_cancel1 = thm"nat_mult_le_cancel1";
    1.92 -val nat_mult_less_cancel1 = thm"nat_mult_less_cancel1";
    1.93 -val nat_mult_eq_cancel1 = thm"nat_mult_eq_cancel1";
    1.94 -val nat_mult_div_cancel1 = thm"nat_mult_div_cancel1";
    1.95 -val nat_mult_le_cancel_disj = thm"nat_mult_le_cancel_disj";
    1.96 -val nat_mult_less_cancel_disj = thm"nat_mult_less_cancel_disj";
    1.97 -val nat_mult_eq_cancel_disj = thm"nat_mult_eq_cancel_disj";
    1.98 -val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj";
    1.99 -
   1.100 -val power_minus_even = thm"power_minus_even";
   1.101 -*}
   1.102 -
   1.103  end