src/HOL/Transcendental.thy
changeset 45308 2e84e5f0463b
parent 44756 efcd71fbaeec
child 45309 5885ec8eb6b0
     1.1 --- a/src/HOL/Transcendental.thy	Sun Oct 30 07:08:33 2011 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Sun Oct 30 09:07:02 2011 +0100
     1.3 @@ -1589,10 +1589,7 @@
     1.4  by simp
     1.5  
     1.6  lemma m2pi_less_pi: "- (2 * pi) < pi"
     1.7 -proof -
     1.8 -  have "- (2 * pi) < 0" and "0 < pi" by auto
     1.9 -  from order_less_trans[OF this] show ?thesis .
    1.10 -qed
    1.11 +by simp
    1.12  
    1.13  lemma sin_pi_half [simp]: "sin(pi/2) = 1"
    1.14  apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
    1.15 @@ -2351,7 +2348,7 @@
    1.16  proof -
    1.17    let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
    1.18    have nonneg: "0 \<le> ?c"
    1.19 -    by (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
    1.20 +    by (simp add: cos_ge_zero)
    1.21    have "0 = cos (pi / 4 + pi / 4)"
    1.22      by simp
    1.23    also have "cos (pi / 4 + pi / 4) = ?c\<twosuperior> - ?s\<twosuperior>"