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