--- a/src/HOL/Library/normarith.ML Fri May 07 10:00:24 2010 +0200
+++ b/src/HOL/Library/normarith.ML Fri May 07 15:05:52 2010 +0200
@@ -168,7 +168,7 @@
val real_poly_conv =
Normalizer.semiring_normalize_wrapper ctxt
(the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
- in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Normalizer.field_comp_conv then_conv real_poly_conv)))
+ in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Numeral_Simprocs.field_comp_conv then_conv real_poly_conv)))
end;
fun absc cv ct = case term_of ct of
@@ -190,8 +190,8 @@
val apply_pth5 = rewr_conv @{thm pth_5};
val apply_pth6 = rewr_conv @{thm pth_6};
val apply_pth7 = rewrs_conv @{thms pth_7};
- val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Normalizer.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
- val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Normalizer.field_comp_conv);
+ val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Numeral_Simprocs.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
+ val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Numeral_Simprocs.field_comp_conv);
val apply_ptha = rewr_conv @{thm pth_a};
val apply_pthb = rewrs_conv @{thms pth_b};
val apply_pthc = rewrs_conv @{thms pth_c};
@@ -204,7 +204,7 @@
| _ => error "headvector: non-canonical term"
fun vector_cmul_conv ct =
- ((apply_pth5 then_conv arg1_conv Normalizer.field_comp_conv) else_conv
+ ((apply_pth5 then_conv arg1_conv Numeral_Simprocs.field_comp_conv) else_conv
(apply_pth6 then_conv binop_conv vector_cmul_conv)) ct
fun vector_add_conv ct = apply_pth7 ct
@@ -396,7 +396,7 @@
fun init_conv ctxt =
Simplifier.rewrite (Simplifier.context ctxt
(HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
- then_conv Normalizer.field_comp_conv
+ then_conv Numeral_Simprocs.field_comp_conv
then_conv nnf_conv
fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);