1.1 --- a/src/HOL/GCD.thy	Tue Oct 25 16:37:11 2011 +0200
     1.2 +++ b/src/HOL/GCD.thy	Thu Oct 27 07:46:57 2011 +0200
     1.3 @@ -357,7 +357,7 @@
     1.4    apply (induct m n rule: gcd_nat_induct)
     1.5    apply simp
     1.6    apply (case_tac "k = 0")
     1.7 -  apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
     1.8 +  apply (simp_all add: gcd_non_0_nat)
     1.9  done
    1.10  
    1.11  lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"

     2.1 --- a/src/HOL/Library/BigO.thy	Tue Oct 25 16:37:11 2011 +0200
     2.2 +++ b/src/HOL/Library/BigO.thy	Thu Oct 27 07:46:57 2011 +0200
     2.3 @@ -129,9 +129,6 @@
     2.4    apply (erule order_trans)
     2.5    apply (simp add: ring_distribs)
     2.6    apply (rule mult_left_mono)
     2.7 -  apply assumption
     2.8 -  apply (simp add: order_less_le)
     2.9 -  apply (rule mult_left_mono)
    2.10    apply (simp add: abs_triangle_ineq)
    2.11    apply (simp add: order_less_le)
    2.12    apply (rule mult_nonneg_nonneg)
    2.13 @@ -150,9 +147,6 @@
    2.14    apply (erule order_trans)
    2.15    apply (simp add: ring_distribs)
    2.16    apply (rule mult_left_mono)
    2.17 -  apply (simp add: order_less_le)
    2.18 -  apply (simp add: order_less_le)
    2.19 -  apply (rule mult_left_mono)
    2.20    apply (rule abs_triangle_ineq)
    2.21    apply (simp add: order_less_le)
    2.22    apply (rule mult_nonneg_nonneg)

     3.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Tue Oct 25 16:37:11 2011 +0200
     3.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Oct 27 07:46:57 2011 +0200
     3.3 @@ -196,9 +196,6 @@
     3.4    apply (erule order_trans)
     3.5    apply (simp add: ring_distribs)
     3.6    apply (rule mult_left_mono)
     3.7 -  apply assumption
     3.8 -  apply (simp add: order_less_le)
     3.9 -  apply (rule mult_left_mono)
    3.10    apply (simp add: abs_triangle_ineq)
    3.11    apply (simp add: order_less_le)
    3.12    apply (rule mult_nonneg_nonneg)
    3.13 @@ -217,9 +214,6 @@
    3.14    apply (erule order_trans)
    3.15    apply (simp add: ring_distribs)
    3.16    apply (rule mult_left_mono)
    3.17 -  apply (simp add: order_less_le)
    3.18 -  apply (simp add: order_less_le)
    3.19 -  apply (rule mult_left_mono)
    3.20    apply (rule abs_triangle_ineq)
    3.21    apply (simp add: order_less_le)
    3.22  apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)

     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 25 16:37:11 2011 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Oct 27 07:46:57 2011 +0200
     4.3 @@ -5298,12 +5298,12 @@
     4.4      then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
     4.5        using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
     4.6      { fix n assume "n\<ge>N"
     4.7 -      hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding f.diff[THEN sym] by auto
     4.8 -      moreover have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
     4.9 +      have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
    4.10          using subspace_sub[OF s, of "x n" "x N"] using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
    4.11          using normf[THEN bspec[where x="x n - x N"]] by auto
    4.12 -      ultimately have "norm (x n - x N) < d" using `e>0`
    4.13 -        using mult_left_less_imp_less[of e "norm (x n - x N)" d] by auto   }
    4.14 +      also have "norm (f (x n - x N)) < e * d"
    4.15 +        using `N \<le> n` N unfolding f.diff[THEN sym] by auto
    4.16 +      finally have "norm (x n - x N) < d" using `e>0` by simp }
    4.17      hence "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" by auto }
    4.18    thus ?thesis unfolding cauchy and dist_norm by auto
    4.19  qed

     5.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Oct 25 16:37:11 2011 +0200
     5.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Thu Oct 27 07:46:57 2011 +0200
     5.3 @@ -134,7 +134,7 @@
     5.4    apply (induct m n rule: gcd_induct)
     5.5     apply simp
     5.6    apply (case_tac "k = 0")
     5.7 -   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
     5.8 +   apply (simp_all add: gcd_non_0)
     5.9    done
    5.10  
    5.11  lemma gcd_mult [simp, algebra]: "gcd k (k * n) = k"

     6.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Oct 25 16:37:11 2011 +0200
     6.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Oct 27 07:46:57 2011 +0200
     6.3 @@ -366,6 +366,7 @@
     6.4    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
     6.5    val simplify_meta_eq  = cancel_simplify_meta_eq
     6.6    val prove_conv = Arith_Data.prove_conv
     6.7 +  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
     6.8  end;
     6.9  
    6.10  structure EqCancelFactor = ExtractCommonTermFun

     7.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Tue Oct 25 16:37:11 2011 +0200
     7.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 27 07:46:57 2011 +0200
     7.3 @@ -512,6 +512,7 @@
     7.4    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
     7.5    val simplify_meta_eq  = cancel_simplify_meta_eq 
     7.6    val prove_conv = Arith_Data.prove_conv
     7.7 +  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
     7.8  end;
     7.9  
    7.10  (*mult_cancel_left requires a ring with no zero divisors.*)

     8.1 --- a/src/HOL/ex/Simproc_Tests.thy	Tue Oct 25 16:37:11 2011 +0200
     8.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Thu Oct 27 07:46:57 2011 +0200
     8.3 @@ -374,9 +374,8 @@
     8.4  lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
     8.5  by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
     8.6  
     8.7 -lemma "(0::rat) < z \<Longrightarrow> z*x < z*y"
     8.8 -apply (tactic {* test [linordered_ring_less_cancel_factor] *})?
     8.9 -oops -- "FIXME: test fails"
    8.10 +lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < z*y"
    8.11 +by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
    8.12  
    8.13  
    8.14  subsection {* @{text linordered_ring_le_cancel_factor} *}
    8.15 @@ -385,8 +384,7 @@
    8.16  by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
    8.17  
    8.18  lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
    8.19 -apply (tactic {* test [linordered_ring_le_cancel_factor] *})?
    8.20 -oops -- "FIXME: test fails"
    8.21 +by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
    8.22  
    8.23  
    8.24  subsection {* @{text field_combine_numerals} *}

     9.1 --- a/src/Provers/Arith/extract_common_term.ML	Tue Oct 25 16:37:11 2011 +0200
     9.2 +++ b/src/Provers/Arith/extract_common_term.ML	Thu Oct 27 07:46:57 2011 +0200
     9.3 @@ -22,6 +22,7 @@
     9.4    val dest_bal: term -> term * term
     9.5    val find_first: term -> term list -> term list
     9.6    (*proof tools*)
     9.7 +  val mk_eq: term * term -> term
     9.8    val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
     9.9    val norm_tac: simpset -> tactic                (*proves the result*)
    9.10    val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*)
    9.11 @@ -65,11 +66,12 @@
    9.12      and terms2' = Data.find_first u terms2
    9.13      and T = Term.fastype_of u
    9.14  
    9.15 +    val t'' = Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2'))
    9.16      val reshape =
    9.17 -      Data.prove_conv [Data.norm_tac ss] ctxt prems
    9.18 -        (t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')))
    9.19 +      Goal.prove ctxt [] [] (Data.mk_eq (t', t'')) (K (Data.norm_tac ss))
    9.20 +
    9.21    in
    9.22 -    Option.map (export o Data.simplify_meta_eq ss simp_th) reshape
    9.23 +    SOME (export (Data.simplify_meta_eq ss simp_th reshape))
    9.24    end
    9.25    (* FIXME avoid handling of generic exceptions *)
    9.26    handle TERM _ => NONE