equal
deleted
inserted
replaced
54 "mult_nat_number_of", "eq_nat_number_of", |
54 "mult_nat_number_of", "eq_nat_number_of", |
55 "less_nat_number_of"] |
55 "less_nat_number_of"] |
56 val powerarith = |
56 val powerarith = |
57 (map thm ["nat_number_of", "zpower_number_of_even", |
57 (map thm ["nat_number_of", "zpower_number_of_even", |
58 "zpower_Pls", "zpower_Min"]) @ |
58 "zpower_Pls", "zpower_Min"]) @ |
59 [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", |
59 [(MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring", |
60 thm "one_eq_Numeral1_nring"] |
60 thm "one_eq_Numeral1_nring"] |
61 (thm "zpower_number_of_odd"))] |
61 (thm "zpower_number_of_odd"))] |
62 |
62 |
63 val comp_arith = binarith @ intarith @ intarithrel @ natarith |
63 val comp_arith = binarith @ intarith @ intarithrel @ natarith |
64 @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"]; |
64 @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"]; |