--- 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