# HG changeset patch
# User himmelma
# Date 1243518164 -7200
# Node ID 4ae81233cf69c57ddd89584a4347f8c0deeeaad7
# Parent  60a53b5af39c5fe85685c5100818e829ea9d0de8
Corrected error in Convex_Euclidean_Space

diff -r 60a53b5af39c -r 4ae81233cf69 src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 13:56:50 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 15:42:44 2009 +0200
@@ -2568,7 +2568,7 @@
 	  finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *s a + (norm (a - x) / norm (a - b)) *s b) $ i" by auto
 	qed(insert Fal2, auto) qed qed
 
-lemma between_midpoint:
+lemma between_midpoint: fixes a::"real^'n::finite" shows
   "between (a,b) (midpoint a b)" (is ?t1) 
   "between (b,a) (midpoint a b)" (is ?t2)
 proof- have *:"\<And>x y z. x = (1/2::real) *s z \<Longrightarrow> y = (1/2) *s z \<Longrightarrow> norm z = norm x + norm y" by auto