# HG changeset patch
# User bauerg
# Date 976902228 -3600
# Node ID 32871d7fbb0aac68c7f9b57505075b3906c32315
# Parent  295a25fee35c66d42b51a3d871ff61b25c01dcd1
corrected errors;

diff -r 295a25fee35c -r 32871d7fbb0a src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Fri Dec 15 18:06:48 2000 +0100
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Fri Dec 15 18:43:48 2000 +0100
@@ -344,16 +344,16 @@
   by (simp add: real_mult_commute)
 
 lemma vs_mult_zero_uniq:
-  "[| is_vectorspace V; x \<in> V; a \<cdot> x = 0; x \<noteq> 0 |] ==> a = #0"
+  "[| is_vectorspace V; x \<in> V; x \<noteq> 0; a \<cdot> x = 0 |] ==> a = 0"
 proof (rule classical)
   assume "is_vectorspace V" "x \<in> V" "a \<cdot> x = 0" "x \<noteq> 0"
-  assume "a \<noteq> #0"
+  assume "a \<noteq> 0"
   have "x = (inverse a * a) \<cdot> x" by (simp!)
   also have "... = inverse a \<cdot> (a \<cdot> x)" by (rule vs_mult_assoc)
   also have "... = inverse a \<cdot> 0" by (simp!)
   also have "... = 0" by (simp!)
   finally have "x = 0" .
-  thus "a = #0" by contradiction 
+  thus "a = 0" by contradiction 
 qed
 
 lemma vs_mult_left_cancel: 
@@ -375,37 +375,14 @@
   "[| is_vectorspace V; x \<in> V; x \<noteq> 0 |] 
   ==> (a \<cdot> x = b \<cdot> x) = (a = b)" (concl is "?L = ?R")
 proof
-  assume "is_vectorspace V" "x \<in> V" "x \<noteq> 0"
+  assume v: "is_vectorspace V" "x \<in> V" "x \<noteq> 0"
   have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x" 
     by (simp! add: vs_diff_mult_distrib2)
   also assume ?L hence "a \<cdot> x - b \<cdot> x = 0" by (simp!)
-  finally have "(a - b) \<cdot> x = 0" . 
-  hence "a - b = #0" by (simp! add: vs_mult_zero_uniq)
-  thus "a = b" by (rule real_add_minus_eq)
-qed simp (*** 
-
-lemma vs_mult_right_cancel: 
-  "[| is_vectorspace V; x:V; x \<noteq> 0 |] ==>  
-  (a ( * ) x = b ( * ) x) = (a = b)"
-  (concl is "?L = ?R");
-proof;
-  assume "is_vectorspace V" "x:V" "x \<noteq> 0";
-  assume l: ?L; 
-  show "a = b"; 
-  proof (rule real_add_minus_eq);
-    show "a - b = (#0::real)"; 
-    proof (rule vs_mult_zero_uniq);
-      have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
-        by (simp! add: vs_diff_mult_distrib2);
-      also; from l; have "a ( * ) x - b ( * ) x = 0"; by (simp!);
-      finally; show "(a - b) ( * ) x  = 0"; .; 
-    qed;
-  qed;
-next;
-  assume ?R;
-  thus ?L; by simp;
-qed;
-**)
+  finally have "(a - b) \<cdot> x = 0" .
+  from v this have "a - b = 0" by (rule vs_mult_zero_uniq) 
+  thus "a = b" by simp
+qed simp 
 
 lemma vs_eq_diff_eq: 
   "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] ==>