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