--- a/src/HOL/Complex/ex/linrtac.ML Mon Jun 11 11:06:13 2007 +0200
+++ b/src/HOL/Complex/ex/linrtac.ML Mon Jun 11 11:06:15 2007 +0200
@@ -18,28 +18,7 @@
"add_BIT_11", "minus_Pls", "minus_Min", "minus_1",
"minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0",
"add_Pls_right", "add_Min_right"];
- val intarithrel =
- (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
- "int_le_number_of_eq","int_iszero_number_of_0",
- "int_less_number_of_eq_neg"]) @
- (map (fn s => thm s RS thm "lift_bool")
- ["int_iszero_number_of_Pls","int_iszero_number_of_1",
- "int_neg_number_of_Min"])@
- (map (fn s => thm s RS thm "nlift_bool")
- ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
-
-val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
- "int_number_of_diff_sym", "int_number_of_mult_sym"];
-val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
- "mult_nat_number_of", "eq_nat_number_of",
- "less_nat_number_of"]
-val powerarith =
- (map thm ["nat_number_of", "zpower_number_of_even",
- "zpower_Pls", "zpower_Min"]) @
- [thm "zpower_number_of_odd"]
-
-val comp_arith = binarith @ intarith @ intarithrel @ natarith
- @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
+val comp_arith = binarith @ simp_thms
val zdvd_int = thm "zdvd_int";
--- a/src/HOL/Complex/ex/mirtac.ML Mon Jun 11 11:06:13 2007 +0200
+++ b/src/HOL/Complex/ex/mirtac.ML Mon Jun 11 11:06:15 2007 +0200
@@ -28,13 +28,6 @@
@{thm "diff_def"}, @{thm "minus_divide_left"}]
val comp_ths = ths @ comp_arith @ simp_thms
-val powerarith =
- (map thm ["nat_number_of", "zpower_number_of_even",
- "zpower_Pls", "zpower_Min"]) @
- [thm "zpower_number_of_odd"]
-
-val comp_arith = comp_ths @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
-
val zdvd_int = @{thm "zdvd_int"};
val zdiff_int_split = @{thm "zdiff_int_split"};
@@ -108,7 +101,7 @@
addsimprocs [cancel_div_mod_proc]
val simpset0 = HOL_basic_ss
addsimps [mod_div_equality', Suc_plus1]
- addsimps comp_arith
+ addsimps comp_ths
addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}]
(* Simp rules for changing (n::int) to int n *)
val simpset1 = HOL_basic_ss
--- a/src/HOL/Real/ferrante_rackoff.ML Mon Jun 11 11:06:13 2007 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML Mon Jun 11 11:06:15 2007 +0200
@@ -25,28 +25,7 @@
"mult_Pls", "mult_Min", "mult_1", "mult_0",
"add_Pls_right", "add_Min_right"];
-val intarithrel =
- map thm ["int_eq_number_of_eq", "int_neg_number_of_BIT", "int_le_number_of_eq",
- "int_iszero_number_of_0", "int_less_number_of_eq_neg"]
- @ map (fn s => thm s RS thm "lift_bool") ["int_iszero_number_of_Pls",
- "int_iszero_number_of_1", "int_neg_number_of_Min"]
- @ map (fn s => thm s RS thm "nlift_bool") ["int_nonzero_number_of_Min",
- "int_not_neg_number_of_Pls"];
-
-val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
- "int_number_of_diff_sym", "int_number_of_mult_sym"];
-
-val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
- "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"];
-
-val powerarith =
- map thm ["nat_number_of", "zpower_number_of_even",
- "zpower_Pls", "zpower_Min"]
- @ [MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
- (thm "zpower_number_of_odd")]
-
-val comp_arith = binarith @ intarith @ intarithrel @ natarith
- @ powerarith @ [thm "not_false_eq_true", thm "not_true_eq_false"];
+val comp_arith = binarith @ arith_simps @ simp_thms
fun prepare_for_linr q fm =
let
--- a/src/HOL/ex/coopertac.ML Mon Jun 11 11:06:13 2007 +0200
+++ b/src/HOL/ex/coopertac.ML Mon Jun 11 11:06:15 2007 +0200
@@ -9,31 +9,7 @@
val nT = HOLogic.natT;
val binarith = map thm
["Pls_0_eq", "Min_1_eq"];
- val intarithrel =
- (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
- "int_le_number_of_eq","int_iszero_number_of_0",
- "int_less_number_of_eq_neg"]) @
- (map (fn s => thm s RS thm "lift_bool")
- ["int_iszero_number_of_Pls","int_iszero_number_of_1",
- "int_neg_number_of_Min"])@
- (map (fn s => thm s RS thm "nlift_bool")
- ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
-
-val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
- "int_number_of_diff_sym", "int_number_of_mult_sym"];
-val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
- "mult_nat_number_of", "eq_nat_number_of",
- "less_nat_number_of"]
-val powerarith =
- (map thm ["nat_number_of", "zpower_number_of_even",
- "zpower_Pls", "zpower_Min"]) @
- [simplify (HOL_basic_ss addsimps [thm "zero_eq_Numeral0_nring",
- thm "one_eq_Numeral1_nring"])
- (thm "zpower_number_of_odd")]
-
-val comp_arith = binarith @ intarith @ intarithrel @ natarith
- @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
-
+val comp_arith = binarith @ simp_thms
val zdvd_int = thm "zdvd_int";
val zdiff_int_split = thm "zdiff_int_split";