diff -r 0e00bc1ad51c -r 2e84e5f0463b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Oct 30 07:08:33 2011 +0100
+++ b/src/HOL/Transcendental.thy	Sun Oct 30 09:07:02 2011 +0100
@@ -1589,10 +1589,7 @@
 by simp
 
 lemma m2pi_less_pi: "- (2 * pi) < pi"
-proof -
-  have "- (2 * pi) < 0" and "0 < pi" by auto
-  from order_less_trans[OF this] show ?thesis .
-qed
+by simp
 
 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
 apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
@@ -2351,7 +2348,7 @@
 proof -
   let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
   have nonneg: "0 \<le> ?c"
-    by (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
+    by (simp add: cos_ge_zero)
   have "0 = cos (pi / 4 + pi / 4)"
     by simp
   also have "cos (pi / 4 + pi / 4) = ?c\<twosuperior> - ?s\<twosuperior>"