src/HOL/ex/coopertac.ML
changeset 23318 6d68b07ab5cf
parent 23274 f997514ad8f4
child 23364 1f3b832c90c1
     1.1 --- a/src/HOL/ex/coopertac.ML	Mon Jun 11 11:06:13 2007 +0200
     1.2 +++ b/src/HOL/ex/coopertac.ML	Mon Jun 11 11:06:15 2007 +0200
     1.3 @@ -9,31 +9,7 @@
     1.4  val nT = HOLogic.natT;
     1.5  val binarith = map thm
     1.6    ["Pls_0_eq", "Min_1_eq"];
     1.7 - val intarithrel = 
     1.8 -     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
     1.9 -		"int_le_number_of_eq","int_iszero_number_of_0",
    1.10 -		"int_less_number_of_eq_neg"]) @
    1.11 -     (map (fn s => thm s RS thm "lift_bool") 
    1.12 -	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
    1.13 -	   "int_neg_number_of_Min"])@
    1.14 -     (map (fn s => thm s RS thm "nlift_bool") 
    1.15 -	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
    1.16 -     
    1.17 -val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
    1.18 -			"int_number_of_diff_sym", "int_number_of_mult_sym"];
    1.19 -val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
    1.20 -			"mult_nat_number_of", "eq_nat_number_of",
    1.21 -			"less_nat_number_of"]
    1.22 -val powerarith = 
    1.23 -    (map thm ["nat_number_of", "zpower_number_of_even", 
    1.24 -	      "zpower_Pls", "zpower_Min"]) @ 
    1.25 -    [simplify (HOL_basic_ss addsimps [thm "zero_eq_Numeral0_nring", 
    1.26 -			   thm "one_eq_Numeral1_nring"])
    1.27 -  (thm "zpower_number_of_odd")]
    1.28 -
    1.29 -val comp_arith = binarith @ intarith @ intarithrel @ natarith 
    1.30 -	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
    1.31 -
    1.32 +val comp_arith = binarith @ simp_thms
    1.33  
    1.34  val zdvd_int = thm "zdvd_int";
    1.35  val zdiff_int_split = thm "zdiff_int_split";