| changeset 57492 | 74bf65a1910a |
| parent 57418 | 6ab1c7cb0b8d |
| child 57512 | cc97b347b301 |
--- a/src/HOL/Transcendental.thy Wed Jul 02 17:34:45 2014 +0200 +++ b/src/HOL/Transcendental.thy Wed Jun 11 14:24:23 2014 +1000 @@ -3046,6 +3046,7 @@ lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y" apply (cut_tac y = y in lemma_tan_total1, auto) + apply hypsubst_thin apply (cut_tac x = xa and y = y in linorder_less_linear, auto) apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0") apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")