| changeset 59872 | db4000b71fdb |
| parent 59720 | f893472fff31 |
| child 60308 | f7e406aba90d |
--- a/src/HOL/Library/ContNotDenum.thy Wed Apr 01 15:47:55 2015 +0100 +++ b/src/HOL/Library/ContNotDenum.thy Wed Apr 01 16:04:21 2015 +0100 @@ -110,7 +110,7 @@ qed lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV" - using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan_tan) + using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan) lemma uncountable_open_interval: fixes a b :: real assumes ab: "a < b"