# HG changeset patch # User wenzelm # Date 1475404353 -7200 # Node ID 2cdc56e8b6712d733ac1f522a1de2bee02a6f24e # Parent ac96fe9224f6d63556c7369f1472dc974b06a5ed tuned; diff -r ac96fe9224f6 -r 2cdc56e8b671 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Oct 02 12:29:18 2016 +0200 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Oct 02 12:32:33 2016 +0200 @@ -817,7 +817,7 @@ openin (subtopology euclidean s) e2 \ s \ e1 \ e2 \ e1 \ e2 = {} \ e1 \ {} \ e2 \ {})" apply (simp add: connected_def openin_open, safe) - apply (simp_all, blast+) \\slow\ + apply (simp_all, blast+) (* SLOW *) done lemma connected_openin_eq: @@ -3693,8 +3693,7 @@ by (metis ball_subset_cball bounded_cball bounded_subset) lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T" - apply (auto simp add: bounded_def) - by (metis Un_iff add_le_cancel_left dist_triangle le_max_iff_disj max.order_iff) + by (auto simp add: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj) lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)" by (induct rule: finite_induct[of F]) auto