# HG changeset patch
# User chaieb
# Date 1181552775 -7200
# Node ID 6d68b07ab5cf3093b92dd27976c49abc5a723ecb
# Parent  90be000da2a71dc89a2da112f0d7cca83e5d51aa
tuned tactic

diff -r 90be000da2a7 -r 6d68b07ab5cf src/HOL/Complex/ex/linrtac.ML
--- 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";
diff -r 90be000da2a7 -r 6d68b07ab5cf src/HOL/Complex/ex/mirtac.ML
--- 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
diff -r 90be000da2a7 -r 6d68b07ab5cf src/HOL/Real/ferrante_rackoff.ML
--- 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
diff -r 90be000da2a7 -r 6d68b07ab5cf src/HOL/ex/coopertac.ML
--- 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";