# HG changeset patch
# User hoelzl
# Date 1450705484 -3600
# Node ID b4bfa62e799dcc7d26e5d2f4899f1a9e25a161d8
# Parent  ff4d33058566de5dbb933ca24f22a245e37d39af
Transcendental: use [simp]-canonical form - (pi/2)

diff -r ff4d33058566 -r b4bfa62e799d src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Dec 17 16:43:36 2015 +0100
+++ b/src/HOL/Transcendental.thy	Mon Dec 21 14:44:44 2015 +0100
@@ -4680,7 +4680,7 @@
   DERIV_arctan[THEN DERIV_chain2, derivative_intros]
   DERIV_arctan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
-lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
+lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- (pi/2)))"
   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
      (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
            intro!: tan_monotone exI[of _ "pi/2"])