--- a/src/HOL/Tools/semiring_normalizer.ML Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Sun Mar 25 20:15:39 2012 +0200
@@ -179,7 +179,7 @@
(case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"),
conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm})
then_conv Simplifier.rewrite (HOL_basic_ss addsimps
- (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))};
+ @{thms numeral_1_eq_1})};
fun field_funs key =
let
@@ -237,13 +237,13 @@
val is_numeral = can dest_numeral;
val numeral01_conv = Simplifier.rewrite
- (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]);
+ (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}]);
val zero1_numeral_conv =
- Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]);
+ Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym]);
fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv;
-val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
- @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"},
- @{thm "less_nat_number_of"}];
+val natarith = [@{thm "numeral_plus_numeral"}, @{thm "diff_nat_numeral"},
+ @{thm "numeral_times_numeral"}, @{thm "numeral_eq_iff"},
+ @{thm "numeral_less_iff"}];
val nat_add_conv =
zerone_conv
@@ -251,7 +251,7 @@
(HOL_basic_ss
addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
@ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
- @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
+ @{thm add_numeral_left}, @{thm Suc_eq_plus1}]
@ map (fn th => th RS sym) @{thms numerals}));
val zeron_tm = @{cterm "0::nat"};