Theorem "arctan" is no longer a default simprule
authorpaulson <lp15@cam.ac.uk>
Wed Apr 01 16:04:21 2015 +0100 (2015-04-01)
changeset 59872db4000b71fdb
parent 59871 e1a49ac9c537
child 59873 2d929c178283
Theorem "arctan" is no longer a default simprule
src/HOL/Library/ContNotDenum.thy
     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"