# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1427900661 -3600
# Node ID db4000b71fdbf445c51fd6b91b6dddca666ba4ef
# Parent  e1a49ac9c537ef3944a2ac10c9e4cfd313b21a43
Theorem "arctan" is no longer a default simprule

diff -r e1a49ac9c537 -r db4000b71fdb src/HOL/Library/ContNotDenum.thy
--- 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"