--- a/src/HOL/Analysis/Derivative.thy Mon Sep 02 19:44:12 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy Wed Sep 04 14:16:27 2019 +0100
@@ -7,7 +7,7 @@
theory Derivative
imports
- Path_Connected
+ Starlike
Operator_Norm
Uniform_Limit
Bounded_Linear_Function
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Mon Sep 02 19:44:12 2019 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Wed Sep 04 14:16:27 2019 +0100
@@ -2,7 +2,7 @@
theory Ordered_Euclidean_Space
imports
- Cartesian_Euclidean_Space
+ Cartesian_Euclidean_Space Path_Connected
"HOL-Library.Product_Order"
begin
--- a/src/HOL/Analysis/Polytope.thy Mon Sep 02 19:44:12 2019 +0200
+++ b/src/HOL/Analysis/Polytope.thy Wed Sep 04 14:16:27 2019 +0100
@@ -3,7 +3,7 @@
text\<open>Ported from HOL Light by L C Paulson\<close>
theory Polytope
-imports Cartesian_Euclidean_Space
+imports Cartesian_Euclidean_Space Path_Connected
begin
subsection \<open>Faces of a (usually convex) set\<close>
@@ -22,9 +22,7 @@
proof -
have *: "\<And>a T S. T face_of S \<Longrightarrow> ((+) a ` T face_of (+) a ` S)"
apply (simp add: face_of_def Ball_def, clarify)
- apply (drule open_segment_translation_eq [THEN iffD1])
- using inj_image_mem_iff inj_add_left apply metis
- done
+ by (meson imageI open_segment_translation_eq)
show ?thesis
apply (rule iffI)
apply (force simp: image_comp o_def dest: * [where a = "-a"])