# HG changeset patch
# User nipkow
# Date 1575045780 -3600
# Node ID a1e94be66bd6c16a86fc9602522e73b2f9ef0e63
# Parent  7fac205dd73725f01081c1dbc6c323c584064cf1
reduced imports; deleted unusewd minor lemmas for that purpose

diff -r 7fac205dd737 -r a1e94be66bd6 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Nov 29 15:06:04 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Nov 29 17:43:00 2019 +0100
@@ -5,7 +5,7 @@
 section \<open>Finite Cartesian Products of Euclidean Spaces\<close>
 
 theory Cartesian_Euclidean_Space
-imports Convex_Euclidean_Space Derivative
+imports Derivative
 begin
 
 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
@@ -450,6 +450,7 @@
   shows "convex {x. \<forall>i. P i (x$i)}"
   using assms unfolding convex_def by auto
 
+(* Unused
 lemma convex_positive_orthant_cart: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
   by (rule convex_box_cart) (simp add: atLeast_def[symmetric])
 
@@ -464,12 +465,12 @@
     where "finite s" "cbox (x - (\<chi> i. d)) (x + (\<chi> i. d)) = convex hull s"
 proof -
   from assms obtain s where "finite s"
-    and "cbox (x - sum ((*\<^sub>R) d) Basis) (x + sum ((*\<^sub>R) d) Basis) = convex hull s"
+    and "cbox (x - sum (( *\<^sub>R) d) Basis) (x + sum (( *\<^sub>R) d) Basis) = convex hull s"
     by (rule cube_convex_hull)
   with that[of s] show thesis
     by (simp add: const_vector_cart)
 qed
-
+*)
 
 subsection "Derivative"