# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1567602987 -3600
# Node ID 0e2a065d6f315c90eb8d32e9e3b597395c408eb9
# Parent  5f4b8a5050901d2f0720d41414cdfe4e3bf77de4
Theory Derivative no longer depends on Path_Connected

diff -r 5f4b8a505090 -r 0e2a065d6f31 src/HOL/Analysis/Derivative.thy
--- 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
diff -r 5f4b8a505090 -r 0e2a065d6f31 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- 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
 
diff -r 5f4b8a505090 -r 0e2a065d6f31 src/HOL/Analysis/Polytope.thy
--- 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"])