1.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu May 06 23:11:57 2010 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu May 06 23:11:57 2010 +0200
     1.3 @@ -1222,7 +1222,7 @@
     1.4     in
     1.5    (let val th = tryfind trivial_axiom (keq @ klep @ kltp)
     1.6     in
     1.7 -    (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th, RealArith.Trivial)
     1.8 +    (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv Normalizer.field_comp_conv) th, RealArith.Trivial)
     1.9     end)
    1.10     handle Failure _ =>
    1.11       (let val proof =

     2.1 --- a/src/HOL/Library/normarith.ML	Thu May 06 23:11:57 2010 +0200
     2.2 +++ b/src/HOL/Library/normarith.ML	Thu May 06 23:11:57 2010 +0200
     2.3 @@ -168,7 +168,7 @@
     2.4    val real_poly_conv = 
     2.5      Normalizer.semiring_normalize_wrapper ctxt
     2.6       (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
     2.7 - in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv)))
     2.8 + 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)))
     2.9  end;
    2.10  
    2.11   fun absc cv ct = case term_of ct of 
    2.12 @@ -190,8 +190,8 @@
    2.13   val apply_pth5 = rewr_conv @{thm pth_5};
    2.14   val apply_pth6 = rewr_conv @{thm pth_6};
    2.15   val apply_pth7 = rewrs_conv @{thms pth_7};
    2.16 - val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
    2.17 - val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv);
    2.18 + 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})));
    2.19 + val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Normalizer.field_comp_conv);
    2.20   val apply_ptha = rewr_conv @{thm pth_a};
    2.21   val apply_pthb = rewrs_conv @{thms pth_b};
    2.22   val apply_pthc = rewrs_conv @{thms pth_c};
    2.23 @@ -204,7 +204,7 @@
    2.24   | _ => error "headvector: non-canonical term"
    2.25  
    2.26  fun vector_cmul_conv ct =
    2.27 -   ((apply_pth5 then_conv arg1_conv field_comp_conv) else_conv
    2.28 +   ((apply_pth5 then_conv arg1_conv Normalizer.field_comp_conv) else_conv
    2.29      (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct
    2.30  
    2.31  fun vector_add_conv ct = apply_pth7 ct 
    2.32 @@ -396,7 +396,7 @@
    2.33    fun init_conv ctxt = 
    2.34     Simplifier.rewrite (Simplifier.context ctxt 
    2.35       (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})))
    2.36 -   then_conv field_comp_conv 
    2.37 +   then_conv Normalizer.field_comp_conv 
    2.38     then_conv nnf_conv
    2.39  
    2.40   fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);

     3.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu May 06 23:11:57 2010 +0200
     3.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu May 06 23:11:57 2010 +0200
     3.3 @@ -751,7 +751,7 @@
     3.4        (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
     3.5       simple_cterm_ord
     3.6  in gen_real_arith ctxt
     3.7 -   (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv,
     3.8 +   (cterm_of_rat, Normalizer.field_comp_conv, Normalizer.field_comp_conv, Normalizer.field_comp_conv,
     3.9      main,neg,add,mul, prover)
    3.10  end;
    3.11  

     4.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu May 06 23:11:57 2010 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu May 06 23:11:57 2010 +0200
     4.3 @@ -2231,7 +2231,7 @@
     4.4      apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof 
     4.5      fix z assume z:"z\<in>{x - ?d..x + ?d}"
     4.6      have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1
     4.7 -      by (metis eq_divide_imp mult_frac_num real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute)
     4.8 +      by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute)
     4.9      show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
    4.10        using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
    4.11    hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption

     5.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu May 06 23:11:57 2010 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu May 06 23:11:57 2010 +0200
     5.3 @@ -810,7 +810,7 @@
     5.4      guess k using real_lbound_gt_zero[OF d[THEN conjunct1] d'[THEN conjunct1]] .. note k=this
     5.5      show ?case apply(rule_tac x=k in exI,rule) defer proof(rule,rule) fix z assume as:"norm(z - y) < k"
     5.6        hence "norm (g z - g y - g' (z - y)) \<le> e / B * norm(g z - g y)" using d' k by auto
     5.7 -      also have "\<dots> \<le> e * norm(z - y)" unfolding mult_frac_num pos_divide_le_eq[OF `B>0`]
     5.8 +      also have "\<dots> \<le> e * norm(z - y)" unfolding times_divide_eq_left pos_divide_le_eq[OF `B>0`]
     5.9  	using lem2[THEN spec[where x=z]] using k as using `e>0` by(auto simp add:field_simps)
    5.10        finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)" by simp qed(insert k, auto) qed qed
    5.11