# HG changeset patch
# User wenzelm
# Date 939393627 -7200
# Node ID fd019ac3485fa6f8e309007e84d0ba7799f43d48
# Parent  6a102f74ad0a6831abaf2694e7190a5a01e53eea
update from Gertrud;

diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,12 +3,21 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+header {* Auxiliary theorems *};
+
 theory Aux = Real + Zorn:;
 
 lemmas [intro!!] = chainD; 
 lemmas chainE2 = chainD2 [elimify];
 lemmas [intro!!] = isLub_isUb;
 
+theorem real_linear_split:
+ "[| x < a ==> Q; x = a ==> Q; a < (x::real) ==> Q |] ==> Q";
+  by (rule real_linear [of x a, elimify], elim disjE, force+);
+
+theorem linorder_linear_split: 
+"[| x < a ==> Q; x = a ==> Q; a < (x::'a::linorder) ==> Q |] ==> Q";
+  by (rule linorder_less_linear [of x a, elimify], elim disjE, force+);
 
 lemma le_max1: "x <= max x (y::'a::linorder)";
   by (simp add: le_max_iff_disj[of x x y]);
@@ -25,160 +34,94 @@
 lemma real_add_minus_eq: "x - y = 0r ==> x = y";
 proof -;
   assume "x - y = 0r";
-  have "x + - y = x - y"; by simp;
-  also; have "... = 0r"; .;
-  finally; have "x + - y = 0r"; .;
+  have "x + - y = 0r"; by (simp!);
   hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
   also; have "... = y"; by simp;
-  finally; show "x = y"; .;
+  finally; show "?thesis"; .;
 qed;
 
 lemma rabs_minus_one: "rabs (- 1r) = 1r"; 
 proof -; 
-  have "rabs (- 1r) = - (- 1r)"; 
-  proof (rule rabs_minus_eqI2);
-    show "-1r < 0r";
-      by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one);
-  qed;
+  have "-1r < 0r"; 
+    by (rule real_minus_zero_less_iff[RS iffD1], simp, 
+        rule real_zero_less_one);
+  hence "rabs (- 1r) = - (- 1r)"; 
+    by (rule rabs_minus_eqI2);
   also; have "... = 1r"; by simp; 
-  finally; show ?thesis; by simp;
+  finally; show ?thesis; .;
 qed;
 
-lemma real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
+lemma real_mult_le_le_mono2: 
+  "[| 0r <= z; x <= y |] ==> x * z <= y * z";
 proof -;
-  assume gz: "0r <= z" and ineq: "x <= y";
+  assume "0r <= z" "x <= y";
   hence "x < y | x = y"; by (force simp add: order_le_less);
   thus ?thesis;
   proof (elim disjE); 
     assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono1);
   next; 
-    assume "x = y"; 
-    hence "x * z <= y * z"; by simp;
-    thus ?thesis; by fast;
+    assume "x = y"; thus ?thesis;; by simp;
   qed;
 qed;
 
-lemma real_mult_less_le_anti: "[| z < 0r; x <= y |] ==> z * y <= z * x";
+lemma real_mult_less_le_anti: 
+  "[| z < 0r; x <= y |] ==> z * y <= z * x";
 proof -;
-  assume lz: "z < 0r" and ineq: "x <= y";
+  assume "z < 0r" "x <= y";
   hence "0r < - z"; by simp;
   hence "0r <= - z"; by (rule real_less_imp_le);
-  with ineq; have "(- z) * x <= (- z) * y"; by (simp add: real_mult_le_le_mono1);
-  hence  "- (z * x) <= - (z * y)"; by (simp add: real_minus_mult_eq1 [RS sym]);
+  hence "(- z) * x <= (- z) * y"; 
+    by (rule real_mult_le_le_mono1);
+  hence  "- (z * x) <= - (z * y)"; 
+    by (simp only: real_minus_mult_eq1);
   thus ?thesis; by simp;
 qed;
 
-lemma real_mult_less_le_mono: "[| 0r < z; x <= y |] ==> z * x <= z * y";
+lemma real_mult_less_le_mono: 
+  "[| 0r < z; x <= y |] ==> z * x <= z * y";
 proof -; 
-  assume gt: "0r < z" and ineq: "x <= y";
-  from gt; have "0r <= z"; by (rule real_less_imp_le);
+  assume "0r < z" "x <= y";
+  have "0r <= z"; by (rule real_less_imp_le);
   thus ?thesis; by (rule real_mult_le_le_mono1); 
 qed;
 
-lemma real_mult_diff_distrib: "a * (- x - (y::real)) = - a * x - a * y";
+lemma real_mult_diff_distrib: 
+  "a * (- x - (y::real)) = - a * x - a * y";
 proof -;
-  have "- x - (y::real) = - x + - y"; by simp;
-  also; have "a * ... = a * - x + a * - y"; by (simp add: real_add_mult_distrib2);
+  have "- x - y = - x + - y"; by simp;
+  also; have "a * ... = a * - x + a * - y"; 
+    by (simp only: real_add_mult_distrib2);
   also; have "... = - a * x - a * y"; 
-    by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1 [RS sym]);
+    by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1);
   finally; show ?thesis; .;
 qed;
 
 lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y";
 proof -; 
-  have "x - (y::real) = x + - y"; by simp;
-  also; have "a * ... = a * x + a * - y"; by (simp add: real_add_mult_distrib2);
+  have "x - y = x + - y"; by simp;
+  also; have "a * ... = a * x + a * - y"; 
+    by (simp only: real_add_mult_distrib2);
   also; have "... = a * x - a * y";   
-    by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1 [RS sym]);
+    by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1);
   finally; show ?thesis; .;
 qed;
 
-lemma le_noteq_imp_less: "[|x <= (r::'a::order); x ~= r |] ==> x < r";
+lemma le_noteq_imp_less: 
+  "[| x <= (r::'a::order); x ~= r |] ==> x < r";
 proof -;
   assume "x <= (r::'a::order)" and ne:"x ~= r";
   then; have "x < r | x = r"; by (simp add: order_le_less);
   with ne; show ?thesis; by simp;
 qed;
 
-lemma minus_le: "- (x::real) <= y ==> - y <= x";
-proof -; 
-  assume "- x <= y";
-  hence "- x < y | - x = y"; by (rule order_le_less [RS iffD1]);
-  thus "-y <= x";
-  proof;
-     assume "- x < y"; show ?thesis; 
-     proof -; 
-       have "- y < - (- x)"; by (rule real_less_swap_iff [RS iffD1]); 
-       hence "- y < x"; by simp;
-       thus ?thesis; by (rule real_less_imp_le);
-    qed;
-  next; 
-     assume "- x = y"; thus ?thesis; by force;
-  qed;
-qed;
+lemma real_minus_le: "- (x::real) <= y ==> - y <= x";
+  by simp;
 
-lemma rabs_interval_iff_1: "(rabs (x::real) <= r) = (-r <= x & x <= r)";
-proof (rule case_split [of "rabs x = r"]);
-  assume  a: "rabs x = r";
-  show ?thesis; 
-  proof;
-    assume "rabs x <= r";
-    show "- r <= x & x <= r";
-    proof;
-      have "- x <= rabs x"; by (rule rabs_ge_minus_self);
-      with a; have "- x <= r"; by simp;
-      thus "- r <= x"; by (simp add : minus_le [of "x" "r"]);
-      have "x <= rabs x"; by (rule rabs_ge_self); 
-      with a; show "x <= r"; by simp; 
-    qed;
-  next; 
-    assume "- r <= x & x <= r";
-    with a; show "rabs x <= r"; by fast;
-  qed;
-next;   
-  assume "rabs x ~= r";
-  show ?thesis; 
-  proof;
-    assume "rabs x <= r"; 
-    have "rabs x < r"; by (rule conjI [RS real_less_le [RS iffD2]]);
-    hence "- r < x & x < r"; by (rule rabs_interval_iff [RS iffD1]);
-    thus "- r <= x & x <= r";
-    proof(elim conjE, intro conjI); 
-      assume "- r < x";
-      show "- r <= x"; by (rule real_less_imp_le); 
-      assume "x < r";
-      show "x <= r"; by (rule real_less_imp_le); 
-    qed;
-  next;
-    assume "- r <= x & x <= r";
-    thus "rabs x <= r";
-    proof; 
-      assume a: "- r <= x" and "x <= r";
-      show ?thesis; 
-      proof (rule rabs_disj [RS disjE, of x]);
-        assume "rabs x = x";
-        thus ?thesis; by simp; 
-      next; 
-        assume "rabs x = - x";
-        with a minus_le [of r x]; show ?thesis; by simp;
-      qed;
-    qed;
-  qed;
-qed;
-
-
-lemma real_diff_ineq_swap: "(d::real) - b <= c + a ==> - a - b <= c - d";
-proof -;
-  assume "d - b <= c + (a::real)";
-  have "- a - b = d - b + (- d - a)"; by (simp!);
-  also; have "... <= c + a + (- d - a)"; by (rule real_add_le_mono1);
-  also; have "... = c - d"; by (simp!);
-  finally; show "- a - b <= c - d"; .;
-qed;
-
+lemma real_diff_ineq_swap: 
+  "(d::real) - b <= c + a ==> - a - b <= c - d";
+  by simp;
 
 lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H";
  by (force simp add: psubset_eq);
 
-
-end;
+end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,10 +3,12 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+header {* Bounds *};
+
 theory Bounds = Main + Real:;
 
 
-section {* The sets of lower and upper bounds *};
+subsection {* The sets of lower and upper bounds *};
 
 constdefs
   is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
@@ -22,10 +24,14 @@
   "UpperBounds A B == Collect (is_UpperBound A B)";
 
 syntax
-  "_UPPERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"     ("(3UPPER'_BOUNDS _:_./ _)" 10)
-  "_UPPERS_U" :: "[pttrn, 'a => bool] => 'a set"           ("(3UPPER'_BOUNDS _./ _)" 10)
-  "_LOWERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"     ("(3LOWER'_BOUNDS _:_./ _)" 10)
-  "_LOWERS_U" :: "[pttrn, 'a => bool] => 'a set"           ("(3LOWER'_BOUNDS _./ _)" 10);
+  "_UPPERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"     
+    ("(3UPPER'_BOUNDS _:_./ _)" 10)
+  "_UPPERS_U" :: "[pttrn, 'a => bool] => 'a set"           
+    ("(3UPPER'_BOUNDS _./ _)" 10)
+  "_LOWERS" :: "[pttrn, 'a set, 'a => bool] => 'a set"     
+    ("(3LOWER'_BOUNDS _:_./ _)" 10)
+  "_LOWERS_U" :: "[pttrn, 'a => bool] => 'a set"           
+    ("(3LOWER'_BOUNDS _./ _)" 10);
 
 translations
   "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (%x. P))"
@@ -34,7 +40,7 @@
   "LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P";
 
 
-section {* Least and greatest elements *};
+subsection {* Least and greatest elements *};
 
 constdefs
   is_Least :: "('a::order) set => 'a => bool"
@@ -50,15 +56,17 @@
   "Greatest B == Eps (is_Greatest B)";
 
 syntax
-  "_LEAST"    :: "[pttrn, 'a => bool] => 'a"   ("(3LLEAST _./ _)" 10)
-  "_GREATEST" :: "[pttrn, 'a => bool] => 'a"   ("(3GREATEST _./ _)" 10);
+  "_LEAST"    :: "[pttrn, 'a => bool] => 'a"  
+    ("(3LLEAST _./ _)" 10)
+  "_GREATEST" :: "[pttrn, 'a => bool] => 'a"  
+    ("(3GREATEST _./ _)" 10);
 
 translations
   "LLEAST x. P" == "Least {x. P}"
   "GREATEST x. P" == "Greatest {x. P}";
 
 
-section {* Inf and Sup *};
+subsection {* Infimum and Supremum *};
 
 constdefs
   is_Sup :: "('a::order) set => 'a set => 'a => bool"
@@ -74,10 +82,14 @@
   "Inf A B == Eps (is_Inf A B)";
 
 syntax
-  "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set"     ("(3SUP _:_./ _)" 10)
-  "_SUP_U" :: "[pttrn, 'a => bool] => 'a set"           ("(3SUP _./ _)" 10)
-  "_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set"     ("(3INF _:_./ _)" 10)
-  "_INF_U" :: "[pttrn, 'a => bool] => 'a set"           ("(3INF _./ _)" 10);
+  "_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set"     
+    ("(3SUP _:_./ _)" 10)
+  "_SUP_U" :: "[pttrn, 'a => bool] => 'a set"           
+    ("(3SUP _./ _)" 10)
+  "_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set"     
+    ("(3INF _:_./ _)" 10)
+  "_INF_U" :: "[pttrn, 'a => bool] => 'a set"           
+    ("(3INF _./ _)" 10);
 
 translations
   "SUP x:A. P" == "Sup A (Collect (%x. P))"
@@ -85,7 +97,6 @@
   "INF x:A. P" == "Inf A (Collect (%x. P))"
   "INF x. P" == "INF x:UNIV. P";
 
-
 lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y";
   by (unfold is_Sup_def, rule isLub_le_isUb);
 
@@ -100,5 +111,4 @@
   finally; show "a <= s"; .;
 qed;
   
-
-end;
+end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,13 +3,15 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+header {* The norm of a function *};
+
 theory FunctionNorm = NormedSpace + FunctionOrder:;
 
 
 constdefs
   is_continous :: "['a set, 'a => real, 'a => real] => bool" 
-  "is_continous V norm f == (is_linearform V f
-                           & (EX c. ALL x:V. rabs (f x) <= c * norm x))";
+  "is_continous V norm f == 
+    (is_linearform V f & (EX c. ALL x:V. rabs (f x) <= c * norm x))";
 
 lemma lipschitz_continousI [intro]: 
   "[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |] 
@@ -19,7 +21,8 @@
   fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
 qed;
   
-lemma continous_linearform [intro!!]: "is_continous V norm f ==> is_linearform V f";
+lemma continous_linearform [intro!!]: 
+  "is_continous V norm f ==> is_linearform V f";
   by (unfold is_continous_def) force;
 
 lemma continous_bounded [intro!!]:
@@ -28,7 +31,8 @@
 
 constdefs
   B:: "[ 'a set, 'a => real, 'a => real ] => real set"
-  "B V norm f == {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm (x)))}";
+  "B V norm f == 
+    {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm (x)))}";
 
 constdefs 
   function_norm :: " ['a set, 'a => real, 'a => real] => real"
@@ -46,10 +50,11 @@
 lemma ex_fnorm [intro!!]: 
   "[| is_normed_vectorspace V norm; is_continous V norm f|]
      ==> is_function_norm V norm f (function_norm V norm f)"; 
-proof (unfold function_norm_def is_function_norm_def is_continous_def Sup_def, elim conjE, 
-    rule selectI2EX);
+proof (unfold function_norm_def is_function_norm_def is_continous_def 
+       Sup_def, elim conjE, rule selectI2EX);
   assume "is_normed_vectorspace V norm";
-  assume "is_linearform V f" and e: "EX c. ALL x:V. rabs (f x) <= c * norm x";
+  assume "is_linearform V f" 
+  and e: "EX c. ALL x:V. rabs (f x) <= c * norm x";
   show  "EX a. is_Sup UNIV (B V norm f) a"; 
   proof (unfold is_Sup_def, rule reals_complete);
     show "EX X. X : B V norm f"; 
@@ -76,10 +81,12 @@
             proof (rule real_rinv_gt_zero);
               show "0r < norm x"; ..;
             qed;
-          qed;
-     (*** or:  by (rule real_less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero); ***)
+          qed;  (*** or:
+          by (rule real_less_imp_le, rule real_rinv_gt_zero, 
+              rule normed_vs_norm_gt_zero); ***)
         qed;
-        also; have "... = c * (norm x * rinv (norm x))"; by (rule real_mult_assoc);
+        also; have "... = c * (norm x * rinv (norm x))"; 
+          by (rule real_mult_assoc);
         also; have "(norm x * rinv (norm x)) = 1r"; 
         proof (rule real_mult_inv_right);
           show "norm x ~= 0r"; 
@@ -88,8 +95,9 @@
             proof (rule lt_imp_not_eq);
               show "0r < norm x"; ..;
             qed;
-          qed;
-     (*** or:  by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero); ***)
+          qed; (*** or:  
+          by (rule not_sym, rule lt_imp_not_eq, 
+              rule normed_vs_norm_gt_zero); ***)
         qed;
         also; have "c * ... = c"; by (simp!);
         also; have "... <= b"; by (simp! add: le_max1);
@@ -101,7 +109,8 @@
   qed;
 qed;
 
-lemma fnorm_ge_zero [intro!!]: "[| is_continous V norm f; is_normed_vectorspace V norm|]
+lemma fnorm_ge_zero [intro!!]: 
+  "[| is_continous V norm f; is_normed_vectorspace V norm|]
    ==> 0r <= function_norm V norm f";
 proof -;
   assume c: "is_continous V norm f" and n: "is_normed_vectorspace V norm";
@@ -126,13 +135,13 @@
         qed;
       qed;
     qed (simp!);
-    from ex_fnorm [OF n c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
+    from ex_fnorm [OF n c]; 
+    show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
       by (simp! add: is_function_norm_def function_norm_def); 
     show "0r : B V norm f"; by (rule B_not_empty);
   qed;
 qed;
   
-
 lemma norm_fx_le_norm_f_norm_x: 
   "[| is_normed_vectorspace V norm; x:V; is_continous V norm f |] 
     ==> rabs (f x) <= (function_norm V norm f) * norm x"; 
@@ -184,9 +193,6 @@
   qed;
 qed;
 
-
-
-
 lemma fnorm_le_ub: 
   "[| is_normed_vectorspace V norm; is_continous V norm f;
      ALL x:V. rabs (f x) <= c * norm x; 0r <= c |]
@@ -198,7 +204,8 @@
          and "0r <= c";
   show "Sup UNIV (B V norm f) <= c"; 
   proof (rule sup_le_ub);
-    from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
+    from ex_fnorm [OF _ c]; 
+    show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
       by (simp! add: is_function_norm_def function_norm_def); 
     show "isUb UNIV (B V norm f) c";  
     proof (intro isUbI setleI ballI);
@@ -217,7 +224,8 @@
             
 	from lt; have "0r < rinv (norm x)";
 	  by (simp! add: real_rinv_gt_zero);
-	then; have inv_leq: "0r <= rinv (norm x)"; by (rule real_less_imp_le);
+	then; have inv_leq: "0r <= rinv (norm x)";
+          by (rule real_less_imp_le);
 
 	from Px; have "y = rabs (f x) * rinv (norm x)"; ..;
 	also; from inv_leq; have "... <= c * norm x * rinv (norm x)";
@@ -235,6 +243,4 @@
   qed;
 qed;
 
-
-end;
-
+end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,10 +3,14 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+header {* An Order on Functions *};
+
 theory FunctionOrder = Subspace + Linearform:;
 
 
-section {* Order on functions *};
+
+subsection {* The graph of a function *}
+
 
 types 'a graph = "('a * real) set";
 
@@ -34,17 +38,20 @@
 lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x";
   by (unfold graph_def, elim CollectE exE) force; 
 
-lemma graph_extD1 [intro!!]: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
+lemma graph_extD1 [intro!!]: 
+  "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
   by (unfold graph_def, force);
 
 lemma graph_extD2 [intro!!]: "[| graph H h <= graph H' h' |] ==> H <= H'";
   by (unfold graph_def, force);
 
-lemma graph_extI: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
+lemma graph_extI: 
+  "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
   by (unfold graph_def, force);
 
 lemma graph_domain_funct: 
-  "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
+  "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) 
+  ==> graph (domain g) (funct g) = g";
 proof (unfold domain_def, unfold funct_def, unfold graph_def, auto);
   fix a b; assume "(a, b) : g";
   show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
@@ -56,6 +63,11 @@
   qed;
 qed;
 
+
+
+subsection {* The set of norm preserving extensions of a function *}
+
+
 constdefs
   norm_pres_extensions :: 
    "['a set, 'a  => real, 'a set, 'a => real] => 'a graph set"
@@ -94,6 +106,5 @@
    ==> (g: norm_pres_extensions E p F f) ";
  by (unfold norm_pres_extensions_def) force;
 
-
 end;
 
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,28 +3,29 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-(*  The proof of two different versions of the Hahn-Banach theorem, 
-    following H. Heuser, Funktionalanalysis, p. 228 - 232. 
-*)
+header {* The Hahn-Banach theorem *};
 
 theory HahnBanach = HahnBanach_lemmas + HahnBanach_h0_lemmas:;
 
+text {*
+  The proof of two different versions of the Hahn-Banach theorem, 
+  following \cite{Heuser}.
+*};
 
-section {* The Hahn-Banach theorem for general linear spaces, 
-     H. Heuser, Funktionalanalysis, p.231 *};
+subsection {* The Hahn-Banach theorem for general linear spaces *};
 
-text  {* Every linear function f on a subspace of E, which is bounded by a quasinorm on E, 
-     can be extended norm preserving to a function on E *};
+text  {* Every linear function f on a subspace of E, which is bounded by a 
+ quasinorm on E, can be extended norm preserving to a function on E *};
 
 theorem hahnbanach: 
-  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
-      ALL x:F. f x <= p x |]
+  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; 
+  is_linearform F f; ALL x:F. f x <= p x |]
   ==> EX h. is_linearform E h
           & (ALL x:F. h x = f x)
           & (ALL x:E. h x <= p x)";
 proof -;
-  assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" "is_linearform F f"
-         "ALL x:F. f x <= p x";
+  assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p"
+         "is_linearform F f" "ALL x:F. f x <= p x";
   
   def M == "norm_pres_extensions E p F f";
  
@@ -36,13 +37,10 @@
     qed;
   qed (blast!)+;
 
+  subsubsect {* Existence of a supremum of the norm preserving functions *}; 
 
-  sect {* Part I b of the proof of the Hahn-Banach Theorem, 
-     H. Heuser, Funktionalanalysis, p.231 *};
-    
-  txt {*  Every chain of norm presenting functions has a supremum in M  *};
-
-  have "!! (c:: 'a graph set). c : chain M ==> EX x. x:c ==> (Union c) : M";  
+  have "!! (c:: 'a graph set). c : chain M ==> EX x. x:c 
+    ==> (Union c) : M";  
   proof -;
     fix c; assume "c:chain M"; assume "EX x. x:c";
     show "(Union c) : M"; 
@@ -53,7 +51,8 @@
               & is_subspace H E 
               & is_subspace F H 
               & (graph F f <= graph H h)
-              & (ALL x::'a:H. h x <= p x)" (is "EX (H::'a set) h::'a => real. ?Q H h");
+              & (ALL x::'a:H. h x <= p x)" 
+      (is "EX (H::'a set) h::'a => real. ?Q H h");
       proof (intro exI conjI);
         let ?H = "domain (Union c)";
         let ?h = "funct (Union c)";
@@ -101,7 +100,8 @@
     thus ?thesis;
     proof (elim exE conjE);
       fix H h; 
-      assume "graph H h = g" "is_linearform (H::'a set) h" "is_subspace H E" "is_subspace F H"
+      assume "graph H h = g" "is_linearform (H::'a set) h" 
+             "is_subspace H E" "is_subspace F H"
       and h_ext: "(graph F f <= graph H h)"
       and h_bound: "ALL x:H. h x <= p x";
 
@@ -110,203 +110,218 @@
         have h: "is_vectorspace H"; ..;
         have f: "is_vectorspace F"; ..;
 
-        sect {* Part I a of the proof of the Hahn-Banach Theorem,
-            H. Heuser, Funktionalanalysis, p.230 *};
-
-        txt {* the maximal norm-preserving function is defined on whole E *};
+subsubsect {* The supremal norm-preserving function is defined on the 
+ whole vectorspace *};
 
-	have eq: "H = E"; 
-	proof (rule classical);
-
-          txt {* assume h is not defined on whole E *};
-
-          assume "H ~= E";
-          show ?thesis; 
-          proof -;
+have eq: "H = E"; 
+proof (rule classical);
 
-            have "EX x:M. g <= x & g ~= x";
-            proof -;
-
-              txt {* h can be extended norm-preserving to H0 *};
+txt {* assume h is not defined on whole E *};
 
-	      have "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M";
-	      proof-;
-                have "H <= E"; ..;
-                hence "H < E"; ..;
-                hence "EX x0:E. x0~:H"; by (rule set_less_imp_diff_not_empty);
-                thus ?thesis;
-                proof;
-                  fix x0; assume "x0:E" "x0~:H";
+  assume "H ~= E";
+  show ?thesis; 
+  proof -;
 
-                  have x0:  "x0 ~= <0>";
-                  proof (rule classical);
-                    presume "x0 = <0>"; 
-                    with h; have "x0:H"; by simp;
-                    thus ?thesis; by contradiction;
-                  qed force;
+    have "EX x:M. g <= x & g ~= x";
+    proof -;
 
-       		  def H0 == "vectorspace_sum H (lin x0)";
-                  have "EX h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M"; 
-                  proof -;
-                    from h; have xi: "EX xi. (ALL y:H. - p (y [+] x0) - h y <= xi) 
-                                   & (ALL y:H. xi <= p (y [+] x0) - h y)"; 
-                    proof (rule ex_xi);
-                      fix u v; assume "u:H" "v:H"; 
-                      show "- p (u [+] x0) - h u <= p (v [+] x0) - h v";
-                      proof (rule real_diff_ineq_swap);
+      txt {* h can be extended norm-preserving to H0 *};
 
-                        show "h v - h u <= p (v [+] x0) + p (u [+] x0)"; 
-                        proof -;
-                          from h; have "h v - h u = h (v [-] u)";
-                             by (simp! add: linearform_diff_linear);
-                          also; from h_bound; have "... <= p (v [-] u)"; by (simp!);
-                          also; have "v [-] u = x0 [+] [-] x0 [+] v [+] [-] u"; 
-                            by (simp! add: vs_add_minus_eq_diff);
-                          also; have "... = v [+] x0 [+] [-] (u [+] x0)"; by (simp!);
-                          also; have "... = (v [+] x0) [-] (u [+] x0)";  
-                            by (simp! only: vs_add_minus_eq_diff);
-                          also; have "p ... <= p (v [+] x0) + p (u [+] x0)"; 
-                            by (rule quasinorm_diff_triangle_ineq) (simp!)+;
-                          finally; show ?thesis; .;
-                        qed;
-                      qed;
-                    qed;
-                    
-                    thus ?thesis;
-                    proof (elim exE, intro exI conjI);
-                      fix xi; assume a: "(ALL y:H. - p (y [+] x0) - h y <= xi) &
-                                         (ALL y:H. xi <= p (y [+] x0) - h y)";
-                      def h0 == "%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H )
-                                            in (h y) + a * xi";
+      have "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 
+                    & graph H0 h0 : M";
+      proof-;
+        have "H <= E"; ..;
+        hence "H < E"; ..;
+        hence "EX x0:E. x0~:H"; 
+          by (rule set_less_imp_diff_not_empty);
+        thus ?thesis;
+        proof;
+          fix x0; assume "x0:E" "x0~:H";
 
-	              have "graph H h <= graph H0 h0"; 
-                      proof (rule graph_extI);
-                        fix t; assume "t:H"; 
-                        show "h t = h0 t";
-                        proof -;
-                          have "(@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
-                            by (rule decomp1, rule x0); 
-                          thus ?thesis; by (simp! add: Let_def);
-                        qed;
-                      next;
-                        show "H <= H0";
-		        proof (rule subspace_subset);
-			  show "is_subspace H H0";
-			  proof (unfold H0_def, rule subspace_vs_sum1);
-			    show "is_vectorspace H"; ..;
-			    show "is_vectorspace (lin x0)"; ..;
-			  qed;
-			qed;
-		      qed;
-                      thus "g <= graph H0 h0"; by (simp!);
-
-                      have "graph H h ~= graph H0 h0";
-                      proof;
-                        assume e: "graph H h = graph H0 h0";
-                        have "x0:H0"; 
-                        proof (unfold H0_def, rule vs_sumI);
-                          show "x0 = <0> [+] x0"; by (simp!);
-                          show "x0 :lin x0"; by (rule x_lin_x);
-                          from h; show "<0> : H"; ..;
-                        qed;
-                        hence "(x0, h0 x0) : graph H0 h0"; by (rule graphI);
-                        with e; have "(x0, h0 x0) : graph H h"; by simp;
-                        hence "x0 : H"; ..;
-                        thus "False"; by contradiction;
-                      qed;
-                      thus "g ~= graph H0 h0"; by (simp!);
-
-                      have "graph H0 h0 : norm_pres_extensions E p F f";
-                      proof (rule norm_pres_extensionI2);
+          have x0:  "x0 ~= <0>";
+          proof (rule classical);
+            presume "x0 = <0>"; 
+            with h; have "x0:H"; by simp;
+            thus ?thesis; by contradiction;
+          qed force;
 
-                        show "is_linearform H0 h0";
-                          by (rule h0_lf, rule x0) (simp!)+;
-
-                        show "is_subspace H0 E";
-                          by (unfold H0_def, rule vs_sum_subspace, rule lin_subspace);
-
-                        show f_h0: "is_subspace F H0";
-                        proof (rule subspace_trans [of F H H0]);
-                          from h lin_vs; have "is_subspace H (vectorspace_sum H (lin x0))"; ..;
-                          thus "is_subspace H H0"; by (unfold H0_def);
-                        qed;
-
-                        show "graph F f <= graph H0 h0";
-                        proof (rule graph_extI);
-                          fix x; assume "x:F";
-                          show "f x = h0 x";
-                          proof -;
-                            have eq: "(@ (y, a). x = y [+] a [*] x0 & y : H) = (x, 0r)";
-                              by (rule decomp1, rule x0) (simp!)+;
+          def H0 == "vectorspace_sum H (lin x0)";
+          have "EX h0. g <= graph H0 h0 & g ~= graph H0 h0 
+                     & graph H0 h0 : M"; 
+          proof -;
+            from h; 
+            have xi: "EX xi. (ALL y:H. - p (y [+] x0) - h y <= xi) 
+                           & (ALL y:H. xi <= p (y [+] x0) - h y)"; 
+            proof (rule ex_xi);
+              fix u v; assume "u:H" "v:H"; 
+              show "- p (u [+] x0) - h u <= p (v [+] x0) - h v";
+              proof (rule real_diff_ineq_swap);
 
-                            have "f x = h x"; ..;
-                            also; have " ... = h x + 0r * xi"; by simp;
-                            also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
-                               by (simp add: Let_def);
-                            also; from eq; 
-                            have "... = (let (y,a) = @ (y,a). x = y [+] a [*] x0 & y : H
-                                          in h y + a * xi)"; by simp;
-                            also; have "... = h0 x"; by (simp!);
-                            finally; show ?thesis; .;
-                          qed;
-                        next;
-                          from f_h0; show "F <= H0"; ..;
-                        qed;
-
-                        show "ALL x:H0. h0 x <= p x";
-                          by (rule h0_norm_pres, rule x0) (assumption | (simp!))+;
-                      qed;
-                      thus "graph H0 h0 : M"; by (simp!);
-                    qed;
-                  qed;
-                  thus ?thesis; ..;
+                show "h v - h u <= p (v [+] x0) + p (u [+] x0)"; 
+                proof -;
+                  from h; have "h v - h u = h (v [-] u)";
+                     by (simp! add: linearform_diff_linear);
+                  also; from h_bound; have "... <= p (v [-] u)"; 
+                    by (simp!);
+                  also; 
+                  have "v [-] u = x0 [+] [-] x0 [+] v [+] [-] u"; 
+                    by (unfold diff_def) (simp!);
+                  also; have "... = v [+] x0 [+] [-] (u [+] x0)"; 
+                    by (simp!);
+                  also; have "... = (v [+] x0) [-] (u [+] x0)";
+                    by (unfold diff_def) (simp!);
+                  also; have "p ... <= p (v [+] x0) + p (u [+] x0)";
+                     by (rule quasinorm_diff_triangle_ineq) 
+                        (simp!)+;
+                  finally; show ?thesis; .;
                 qed;
               qed;
+            qed;
+            
+            thus ?thesis;
+            proof (elim exE, intro exI conjI);
+              fix xi; 
+              assume a: "(ALL y:H. - p (y [+] x0) - h y <= xi) 
+                        & (ALL y:H. xi <= p (y [+] x0) - h y)";
+              def h0 == 
+                "%x. let (y,a) = @(y,a). (x = y [+] a [*] x0 & y:H )
+                     in (h y) + a * xi";
 
-              thus ?thesis;
-                by (elim exE conjE, intro bexI conjI);
-            qed;
-            hence "~ (ALL x:M. g <= x --> g = x)"; by force;
-            thus ?thesis; by contradiction;
-          qed;
-	qed; 
+	      have "graph H h <= graph H0 h0"; 
+              proof (rule graph_extI);
+                fix t; assume "t:H"; 
+                show "h t = h0 t";
+                proof -;
+                  have "(@ (y, a). t = y [+] a [*] x0 & y : H) 
+                         = (t,0r)";
+                    by (rule decomp1, rule x0); 
+                  thus ?thesis; by (simp! add: Let_def);
+                qed;
+              next;
+                show "H <= H0";
+		proof (rule subspace_subset);
+	          show "is_subspace H H0";
+		  proof (unfold H0_def, rule subspace_vs_sum1);
+		    show "is_vectorspace H"; ..;
+		    show "is_vectorspace (lin x0)"; ..;
+		  qed;
+		qed;
+	      qed;
+              thus "g <= graph H0 h0"; by (simp!);
+
+              have "graph H h ~= graph H0 h0";
+              proof;
+                assume e: "graph H h = graph H0 h0";
+                have "x0:H0"; 
+                proof (unfold H0_def, rule vs_sumI);
+                  show "x0 = <0> [+] x0"; by (simp!);
+                  show "x0 :lin x0"; by (rule x_lin_x);
+                  from h; show "<0> : H"; ..;
+                qed;
+                hence "(x0, h0 x0) : graph H0 h0"; by (rule graphI);
+                with e; have "(x0, h0 x0) : graph H h"; by simp;
+                hence "x0 : H"; ..;
+                thus "False"; by contradiction;
+              qed;
+              thus "g ~= graph H0 h0"; by (simp!);
+
+              have "graph H0 h0 : norm_pres_extensions E p F f";
+              proof (rule norm_pres_extensionI2);
+
+                show "is_linearform H0 h0";
+                  by (rule h0_lf, rule x0) (simp!)+;
+
+                show "is_subspace H0 E";
+                  by (unfold H0_def, rule vs_sum_subspace, 
+                     rule lin_subspace);
 
-        show "is_linearform E h & (ALL x:F. h x = f x) & (ALL x:E. h x <= p x)";
-        proof (intro conjI); 
-          from eq; show "is_linearform E h"; by (simp!);
-          show "ALL x:F. h x = f x"; 
-          proof (intro ballI, rule sym);
-            fix x; assume "x:F"; show "f x = h x "; ..;
+                show f_h0: "is_subspace F H0";
+                proof (rule subspace_trans [of F H H0]);
+                  from h lin_vs; 
+                  have "is_subspace H (vectorspace_sum H (lin x0))"; 
+                    ..;
+                  thus "is_subspace H H0"; by (unfold H0_def);
+                qed;
+
+                show "graph F f <= graph H0 h0";
+                proof (rule graph_extI);
+                  fix x; assume "x:F";
+                  show "f x = h0 x";
+                  proof -;
+                    have eq: 
+                      "(@(y, a). x = y [+] a [*] x0 & y : H) 
+                        = (x, 0r)";
+                      by (rule decomp1, rule x0) (simp!)+;
+
+                    have "f x = h x"; ..;
+                    also; have " ... = h x + 0r * xi"; by simp;
+                    also; have 
+                       "... = (let (y,a) = (x, 0r) in h y + a * xi)";
+                       by (simp add: Let_def);
+                    also; from eq; have 
+                      "... = (let (y,a) = @ (y,a). 
+                                          x = y [+] a [*] x0 & y : H
+                            in h y + a * xi)"; by simp;
+                    also; have "... = h0 x"; by (simp!);
+                    finally; show ?thesis; .;
+                  qed;
+                next;
+                  from f_h0; show "F <= H0"; ..;
+                qed;
+
+                show "ALL x:H0. h0 x <= p x";
+                  by (rule h0_norm_pres, rule x0) 
+                     (assumption | (simp!))+;
+              qed;
+              thus "graph H0 h0 : M"; by (simp!);
+            qed;
           qed;
-          from eq; show "ALL x:E. h x <= p x"; by (force!);
+          thus ?thesis; ..;
         qed;
-      qed;  
-    qed; 
+      qed;
+
+      thus ?thesis;
+        by (elim exE conjE, intro bexI conjI);
+    qed;
+    hence "~ (ALL x:M. g <= x --> g = x)"; by force;
+    thus ?thesis; by contradiction;
   qed;
+qed; 
+
+show "is_linearform E h & (ALL x:F. h x = f x) 
+     & (ALL x:E. h x <= p x)";
+proof (intro conjI); 
+  from eq; show "is_linearform E h"; by (simp!);
+  show "ALL x:F. h x = f x"; 
+  proof (intro ballI, rule sym);
+    fix x; assume "x:F"; show "f x = h x "; ..;
+  qed;
+  from eq; show "ALL x:E. h x <= p x"; by (force!);
+qed; 
+qed; 
+qed; 
+qed; 
 qed;
 
-
-section  {* Part I (for real linear spaces) of the proof of the Hahn-banach Theorem,
-   H. Heuser, Funktionalanalysis, p.229 *};
-
-text {* Alternative Formulation of the theorem *};
+subsection  {* Alternative formulation of the theorem *};
 
 theorem rabs_hahnbanach:
-  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
-     ALL x:F. rabs (f x) <= p x |]
- ==> EX g. is_linearform E g
-         & (ALL x:F. g x = f x)
-         & (ALL x:E. rabs (g x) <= p x)";
+  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; 
+  is_linearform F f; ALL x:F. rabs (f x) <= p x |]
+  ==> EX g. is_linearform E g
+          & (ALL x:F. g x = f x)
+          & (ALL x:E. rabs (g x) <= p x)";
 proof -; 
-
-  assume e: "is_vectorspace E" and  "is_subspace F E" "is_quasinorm E p" "is_linearform F f" 
-         "ALL x:F. rabs (f x) <= p x";
+  assume e: "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" 
+            "is_linearform F f"  "ALL x:F. rabs (f x) <= p x";
   have "ALL x:F. f x <= p x"; by (rule rabs_ineq [RS iffD1]);
-  hence  "EX g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. g x <= p x)";
+  hence "EX g. is_linearform E g & (ALL x:F. g x = f x) 
+              & (ALL x:E. g x <= p x)";
     by (simp! only: hahnbanach);
   thus ?thesis;
   proof (elim exE conjE);
-    fix g; assume "is_linearform E g" "ALL x:F. g x = f x" "ALL x:E. g x <= p x";
+    fix g; assume "is_linearform E g" "ALL x:F. g x = f x" 
+                  "ALL x:E. g x <= p x";
     show ?thesis;
     proof (intro exI conjI)+;
       from e; show "ALL x:E. rabs (g x) <= p x"; 
@@ -316,8 +331,7 @@
 qed;
 
 
-section {* The Hahn-Banach theorem for normd spaces, 
-     H. Heuser, Funktionalanalysis, p.232 *};
+subsection {* The Hahn-Banach theorem for normed spaces *};
 
 text  {* Every continous linear function f on a subspace of E, 
      can be extended to a continous function on E with the same norm *};
@@ -330,9 +344,7 @@
          & (ALL x:F. g x = f x) 
          & function_norm E norm g = function_norm F norm f"
   (concl is "EX g::'a=>real. ?P g");
-
 proof -;
-
   assume a: "is_normed_vectorspace E norm";
   assume b: "is_subspace F E" "is_linearform F f";
   assume c: "is_continous F norm f";
@@ -341,7 +353,8 @@
 
   def p == "%x::'a. (function_norm F norm f) * norm x";
   
-  let ?P' = "%g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. rabs (g x) <= p x)";
+  let ?P' = "%g. is_linearform E g & (ALL x:F. g x = f x) 
+              & (ALL x:E. rabs (g x) <= p x)";
 
   have q: "is_quasinorm E p";
   proof;
@@ -355,9 +368,12 @@
 
     show "p (a [*] x) = (rabs a) * (p x)";
     proof -; 
-      have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)"; by (simp!);
-      also; have "norm (a [*] x) = rabs a * norm x"; by (rule normed_vs_norm_mult_distrib);
-      also; have "(function_norm F norm f) * ... = rabs a * ((function_norm F norm f) * norm x)";
+      have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)"; 
+        by (simp!);
+      also; have "norm (a [*] x) = rabs a * norm x"; 
+        by (rule normed_vs_norm_mult_distrib);
+      also; have "(function_norm F norm f) * ... 
+        = rabs a * ((function_norm F norm f) * norm x)";
         by (simp! only: real_mult_left_commute);
       also; have "... = (rabs a) * (p x)"; by (simp!);
       finally; show ?thesis; .;
@@ -365,13 +381,15 @@
 
     show "p (x [+] y) <= p x + p y";
     proof -;
-      have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)"; by (simp!);
-      also; have "... <=  (function_norm F norm f) * (norm x + norm y)";
+      have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)"; 
+        by (simp!);
+      also; have "... <= (function_norm F norm f) * (norm x + norm y)";
       proof (rule real_mult_le_le_mono1);
         from _ f; show "0r <= function_norm F norm f"; ..;
         show "norm (x [+] y) <= norm x + norm y"; ..;
       qed;
-      also; have "... = (function_norm F norm f) * (norm x) + (function_norm F norm f) * (norm y)";
+      also; have "... = (function_norm F norm f) * (norm x) 
+                        + (function_norm F norm f) * (norm y)";
         by (simp! only: real_add_mult_distrib2);
       finally; show ?thesis; by (simp!);
     qed;
@@ -380,7 +398,8 @@
   have "ALL x:F. rabs (f x) <= p x";
   proof;
     fix x; assume "x:F";
-     from f; show "rabs (f x) <= p x"; by (simp! add: norm_fx_le_norm_f_norm_x);
+     from f; show "rabs (f x) <= p x"; 
+       by (simp! add: norm_fx_le_norm_f_norm_x);
   qed;
 
   with e b q; have "EX g. ?P' g";
@@ -389,7 +408,8 @@
   thus "?thesis";
   proof (elim exE conjE, intro exI conjI);
     fix g;
-    assume "is_linearform E g" and a: "ALL x:F. g x = f x" and "ALL x:E. rabs (g x) <= p x";
+    assume "is_linearform E g" and a: "ALL x:F. g x = f x" 
+       and "ALL x:E. rabs (g x) <= p x";
     show ce: "is_continous E norm g";
     proof (rule lipschitz_continousI);
       fix x; assume "x:E";
@@ -398,7 +418,8 @@
     qed;
     show "function_norm E norm g = function_norm F norm f";
     proof (rule order_antisym);
-      from _ ce; show "function_norm E norm g <= function_norm F norm f";
+      from _ ce; 
+      show "function_norm E norm g <= function_norm F norm f";
       proof (rule fnorm_le_ub);
         show "ALL x:E. rabs (g x) <=  function_norm F norm f * norm x";
         proof;
@@ -415,14 +436,16 @@
           fix x; assume "x : F"; 
           from a; have "g x = f x"; ..;
           hence "rabs (f x) = rabs (g x)"; by simp;
-          also; from _ _ ce; have "... <= function_norm E norm g * norm x"; 
+          also; from _ _ ce; 
+          have "... <= function_norm E norm g * norm x"; 
           proof (rule norm_fx_le_norm_f_norm_x);
             show "x : E";
             proof (rule subsetD); 
               show "F <= E"; ..;
             qed;
           qed;
-          finally; show "rabs (f x) <= function_norm E norm g * norm x"; .;
+          finally; 
+          show "rabs (f x) <= function_norm E norm g * norm x"; .;
         qed;
         from _ e; show "is_normed_vectorspace F norm"; ..;
         from ce; show "0r <= function_norm E norm g"; ..;
@@ -431,6 +454,4 @@
   qed;
 qed;
 
-
-end;
-
+end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach_h0_lemmas.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,11 +3,14 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+header {* Lemmas about the extension of a non-maximal function *};
+
 theory HahnBanach_h0_lemmas = FunctionNorm:;
 
-
-lemma ex_xi: "[| is_vectorspace F;  (!! u v. [| u:F; v:F |] ==> a u <= b v )|]
-       ==> EX xi::real. (ALL y:F. (a::'a => real) y <= xi) & (ALL y:F. xi <= b y)"; 
+lemma ex_xi: 
+  "[| is_vectorspace F;  (!! u v. [| u:F; v:F |] ==> a u <= b v )|]
+  ==> EX xi::real. (ALL y:F. (a::'a => real) y <= xi) 
+                 & (ALL y:F. xi <= b y)"; 
 proof -;
   assume vs: "is_vectorspace F";
   assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
@@ -74,17 +77,19 @@
   qed;
 qed;
 
-
 lemma h0_lf: 
-  "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi);
-      H0 = vectorspace_sum H (lin x0); is_subspace H E; is_linearform H h; x0 ~: H; 
-      x0 : E; x0 ~= <0>; is_vectorspace E |]
-    ==> is_linearform H0 h0";
+  "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
+                in (h y) + a * xi);
+  H0 = vectorspace_sum H (lin x0); is_subspace H E; is_linearform H h; 
+  x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E |]
+  ==> is_linearform H0 h0";
 proof -;
-  assume h0_def:  "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi)"
-    and H0_def: "H0 = vectorspace_sum H (lin x0)"
-    and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H" "x0 ~= <0>" "x0 : E" 
-            "is_vectorspace E";
+  assume h0_def: 
+    "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
+               in (h y) + a * xi)"
+  and H0_def: "H0 = vectorspace_sum H (lin x0)"
+  and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H" "x0 ~= <0>" 
+          "x0 : E" "is_vectorspace E";
 
   have h0: "is_vectorspace H0"; 
   proof (simp only: H0_def, rule vs_sum_vs);
@@ -101,7 +106,7 @@
       by (simp add: H0_def vectorspace_sum_def lin_def) blast;
     from x2; have ex_x2: "? y2 a2. (x2 = y2 [+] a2 [*] x0 & y2 : H)"; 
       by (simp add: H0_def vectorspace_sum_def lin_def) blast;
-    from x1x2; have ex_x1x2: "? y a. (x1 [+] x2 = y [+] a [*] x0  & y : H)";    
+    from x1x2; have ex_x1x2: "? y a. (x1 [+] x2 = y [+] a [*] x0  & y : H)";
       by (simp add: H0_def vectorspace_sum_def lin_def) force;
     from ex_x1 ex_x2 ex_x1x2;
     show "h0 (x1 [+] x2) = h0 x1 + h0 x2";
@@ -116,9 +121,12 @@
         show "y1 [+] y2 [+] (a1 + a2) [*] x0 = y [+] a [*] x0"; 
         proof -;
           have "y [+] a [*] x0 = x1 [+] x2"; by (rule sym);
-          also; from y1 y2; have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by simp; 
-          also; from vs y1' y2'; have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)"; by simp;
-          also; from vs y1' y2'; have "... = y1 [+] y2 [+] (a1 + a2) [*] x0"; 
+          also; from y1 y2; 
+          have "... = y1 [+] a1 [*] x0 [+] (y2 [+] a2 [*] x0)"; by simp; 
+          also; from vs y1' y2'; 
+          have "... = y1 [+] y2 [+] (a1 [*] x0 [+] a2 [*] x0)"; by simp;
+          also; from vs y1' y2'; 
+          have "... = y1 [+] y2 [+] (a1 + a2) [*] x0"; 
             by (simp add: vs_add_mult_distrib2[of E]);
           finally; show ?thesis; by (rule sym);
         qed;
@@ -145,7 +153,8 @@
       by (rule vs_mult_closed, rule h0);
     from x1; have ex_x1: "? y1 a1. (x1 = y1 [+] a1 [*] x0 & y1 : H)";
       by (simp add: H0_def vectorspace_sum_def lin_def, fast);
-    from x1; have ex_x: "!! x. x: H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)"; 
+    from x1; 
+    have ex_x: "!! x. x: H0 ==> ? y a. (x = y [+] a [*] x0 & y : H)"; 
       by (simp add: H0_def vectorspace_sum_def lin_def, fast);
     note ex_ax1 = ex_x [of "c [*] x1", OF ax1];
     from ex_x1 ex_ax1; show "h0 (c [*] x1) = c * (h0 x1)";  
@@ -162,7 +171,8 @@
           also; from y1; have "... = c [*] (y1 [+] a1 [*] x0)"; by simp;
           also; from vs y1'; have "... = c [*] y1 [+] c [*] (a1 [*] x0)"; 
             by (simp add: vs_add_mult_distrib1);
-          also; from vs y1'; have "... = c [*] y1 [+] (c * a1) [*] x0"; by simp;
+          also; from vs y1'; have "... = c [*] y1 [+] (c * a1) [*] x0"; 
+            by simp;
           finally; show ?thesis; by (rule sym);
         qed;
         show "c [*] y1: H"; ..;
@@ -184,28 +194,23 @@
   qed;
 qed;
 
-
-theorem real_linear_split:
- "[| x < a ==> Q; x = a ==> Q; a < (x::real) ==> Q |] ==> Q";
-  by (rule real_linear [of x a, elimify], elim disjE, force+);
-
-theorem linorder_linear_split: 
-"[| x < a ==> Q; x = a ==> Q; a < (x::'a::linorder) ==> Q |] ==> Q";
-  by (rule linorder_less_linear [of x a, elimify], elim disjE, force+);
-
-
 lemma h0_norm_pres:
-    "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi);
-      H0 = vectorspace_sum H (lin x0); x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E; 
-      is_subspace H E; is_quasinorm E p; is_linearform H h; ALL y:H. h y <= p y;
-      (ALL y:H. - p (y [+] x0) - h y <= xi) & (ALL y:H. xi <= p (y [+] x0) - h y)|]
+  "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
+                in (h y) + a * xi);
+  H0 = vectorspace_sum H (lin x0); x0 ~: H; x0 : E; x0 ~= <0>; 
+  is_vectorspace E; is_subspace H E; is_quasinorm E p; is_linearform H h; 
+  ALL y:H. h y <= p y;
+  (ALL y:H. - p (y [+] x0) - h y <= xi) 
+  & (ALL y:H. xi <= p (y [+] x0) - h y)|]
    ==> ALL x:H0. h0 x <= p x"; 
 proof; 
-  assume h0_def: "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi)"
-     and H0_def: "H0 = vectorspace_sum H (lin x0)" 
-     and vs:     "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E" 
-                 "is_subspace H E" "is_quasinorm E p" "is_linearform H h" 
-     and a:      " ALL y:H. h y <= p y";
+  assume h0_def: 
+    "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
+               in (h y) + a * xi)"
+    and H0_def: "H0 = vectorspace_sum H (lin x0)" 
+    and vs:     "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E" 
+                "is_subspace H E" "is_quasinorm E p" "is_linearform H h" 
+    and a:      " ALL y:H. h y <= p y";
   presume a1: "(ALL y:H. - p (y [+] x0) - h y <= xi)";
   presume a2: "(ALL y:H. xi <= p (y [+] x0) - h y)";
   fix x; assume "x : H0"; 
@@ -227,10 +232,12 @@
           assume lz: "a < 0r"; hence nz: "a ~= 0r"; by force;
           show ?thesis;
           proof -;
-            from a1; have "- p (rinv a [*] y [+] x0) - h (rinv a [*] y) <= xi";
+            from a1; 
+            have "- p (rinv a [*] y [+] x0) - h (rinv a [*] y) <= xi";
               by (rule bspec, simp!);
             
-            with lz; have "a * xi <= a * (- p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
+            with lz; 
+            have "a * xi <= a * (- p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
               by (rule real_mult_less_le_anti);
             also; have "... = - a * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
               by (rule real_mult_diff_distrib);
@@ -257,12 +264,15 @@
           assume gz: "0r < a"; hence nz: "a ~= 0r"; by force;
           show ?thesis;
           proof -;
-            from a2; have "xi <= p (rinv a [*] y [+] x0) - h (rinv a [*] y)";
-            by (rule bspec, simp!);
+            from a2; 
+            have "xi <= p (rinv a [*] y [+] x0) - h (rinv a [*] y)";
+              by (rule bspec, simp!);
 
-            with gz; have "a * xi <= a * (p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
+            with gz; 
+            have "a * xi <= a * (p (rinv a [*] y [+] x0) - h (rinv a [*] y))";
               by (rule real_mult_less_le_mono);
-            also; have "... = a * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
+            also; 
+            have "... = a * (p (rinv a [*] y [+] x0)) - a * (h (rinv a [*] y))";
               by (rule real_mult_diff_distrib2); 
             also; from gz vs y; 
             have "a * (p (rinv a [*] y [+] x0)) = p (a [*] (rinv a [*] y [+] x0))";
@@ -287,5 +297,4 @@
   qed; 
 qed blast+;
 
-
 end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach_lemmas.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,13 +3,17 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+header {* Lemmas about the supremal function w.r.t.~the function order *};
+
 theory HahnBanach_lemmas = FunctionNorm + Zorn_Lemma:;
 
-
-lemma rabs_ineq: "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; is_linearform H h |] \
- \ ==>  (ALL x:H. rabs (h x) <= p x)  = ( ALL x:H. h x <= p x)" (concl is "?L = ?R");
+lemma rabs_ineq: 
+  "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; is_linearform H h |] 
+  ==>  (ALL x:H. rabs (h x) <= p x)  = ( ALL x:H. h x <= p x)" 
+  (concl is "?L = ?R");
 proof -;
-  assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p" "is_linearform H h";
+  assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p" 
+         "is_linearform H h";
   have h: "is_vectorspace H"; ..;
   show ?thesis;
   proof; 
@@ -30,12 +34,14 @@
       show "rabs (h x) <= p x"; 
       proof -; 
         show "!! r x. [| - r <= x; x <= r |] ==> rabs x <= r";
-          by (simp add: rabs_interval_iff_1);
-	show "- p x <= h x";  thm minus_le;
-	proof (rule minus_le);
-	  from h; have "- h x = h ([-] x)"; by (rule linearform_neg_linear [RS sym]);
+          by arith;
+	show "- p x <= h x";
+	proof (rule real_minus_le);
+	  from h; have "- h x = h ([-] x)"; 
+            by (rule linearform_neg_linear [RS sym]);
 	  also; from r; have "... <= p ([-] x)"; by (simp!);
-	  also; have "... = p x"; by (rule quasinorm_minus, rule subspace_subsetD);
+	  also; have "... = p x"; 
+            by (rule quasinorm_minus, rule subspace_subsetD);
 	  finally; show "- h x <= p x"; .; 
 	qed;
 	from r; show "h x <= p x"; ..; 
@@ -45,10 +51,12 @@
 qed;  
 
 lemma  some_H'h't:
-  "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; x:H|]
-   ==> EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c & t:graph H' h' &
-                       is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
-                       (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
+  "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; 
+  x:H|]
+   ==> EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c 
+                 & t:graph H' h' & is_linearform H' h' & is_subspace H' E 
+                 & is_subspace F H' & (graph F f <= graph H' h') 
+                 & (ALL x:H'. h' x <= p x)";
 proof -;
   assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M" 
      and u: "graph H h = Union c" "x:H";
@@ -72,16 +80,18 @@
       from cM; have "c <= M"; by (rule chainD2);
       hence "g : M"; ..;
       hence "g : norm_pres_extensions E p F f"; by (simp only: m);
-      hence "EX H' h'. graph H' h' = g & ?P H' h'"; by (rule norm_pres_extension_D);
+      hence "EX H' h'. graph H' h' = g & ?P H' h'"; 
+        by (rule norm_pres_extension_D);
       thus ?thesis; by (elim exE conjE, intro exI conjI) (simp | simp!)+;
     qed;
   qed;
 qed;
       
-lemma some_H'h': "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; x:H|] 
- ==> EX H' h'. x:H' & (graph H' h' <= graph H h) & 
-               is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
-               (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
+lemma some_H'h': "[| M = norm_pres_extensions E p F f; c: chain M; 
+  graph H h = Union c; x:H|] 
+  ==> EX H' h'. x:H' & (graph H' h' <= graph H h) & 
+                is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
+                (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
 proof -;
   assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M" 
      and u: "graph H h = Union c" "x:H";  
@@ -100,25 +110,29 @@
                    & is_subspace H' E
                    & is_subspace F H'
                    & (graph F f <= graph H' h')
-                   & (ALL x:H'. h' x <= p x)"; by (rule norm_pres_extension_D);
+                   & (ALL x:H'. h' x <= p x)"; 
+      by (rule norm_pres_extension_D);
     thus ?thesis; 
     proof (elim exE conjE, intro exI conjI);
       fix H' h'; assume g': "graph H' h' = g";
       with g; have "(x, h x): graph H' h'"; by simp;
       thus "x:H'"; by (rule graphD1);
       from g g'; have "graph H' h' : c"; by simp;
-      with cM u; show "graph H' h' <= graph H h"; by (simp only: chain_ball_Union_upper);
+      with cM u; show "graph H' h' <= graph H h"; 
+        by (simp only: chain_ball_Union_upper);
     qed simp+;
   qed;
 qed;
 
 lemma some_H'h'2: 
-  "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; x:H; y:H|] 
-  ==> EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h)
-                & is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
+  "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; 
+  x:H; y:H|] 
+  ==> EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) 
+  & is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
                 (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
 proof -;
-  assume "M = norm_pres_extensions E p F f" "c: chain M" "graph H h = Union c";
+  assume "M = norm_pres_extensions E p F f" "c: chain M" 
+         "graph H h = Union c";
  
   let ?P = "%H h. is_linearform H h 
                     & is_subspace H E 
@@ -126,12 +140,12 @@
                     & (graph F f <= graph H h)
                     & (ALL x:H. h x <= p x)";
   assume "x:H";
-  have e1: "EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c & t:graph H' h' &
-                        ?P H' h'";
+  have e1: "EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c 
+                      & t:graph H' h' & ?P H' h'";
     by (rule some_H'h't); 
   assume "y:H";
-  have e2: "EX H' h' t. t : (graph H h) & t = (y, h y) & (graph H' h'):c & t:graph H' h' & 
-                        ?P H' h'";
+  have e2: "EX H' h' t. t : (graph H h) & t = (y, h y) & (graph H' h'):c 
+                      & t:graph H' h' & ?P H' h'";
     by (rule some_H'h't); 
 
   from e1 e2; show ?thesis; 
@@ -147,7 +161,8 @@
            "graph F f <= graph H' h'"   "graph F f <= graph H'' h''"
            "ALL x:H'. h' x <= p x"      "ALL x:H''. h'' x <= p x";
 
-    have "(graph H'' h'') <= (graph H' h') | (graph H' h') <= (graph H'' h'')";
+    have "(graph H'' h'') <= (graph H' h') 
+         | (graph H' h') <= (graph H'' h'')";
       by (rule chainD);
     thus "?thesis";
     proof; 
@@ -179,15 +194,18 @@
   qed;
 qed;
 
-lemma sup_uniq: "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
-       ALL x:F. f x <= p x; M == norm_pres_extensions E p F f; c : chain M;
-       EX x. x : c; (x, y) : Union c; (x, z) : Union c |]
-     ==> z = y";
+lemma sup_uniq: 
+  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; 
+  is_linearform F f; ALL x:F. f x <= p x; M == norm_pres_extensions E p F f;
+   c : chain M; EX x. x : c; (x, y) : Union c; (x, z) : Union c |]
+   ==> z = y";
 proof -;
-  assume "M == norm_pres_extensions E p F f" "c : chain M" "(x, y) : Union c" " (x, z) : Union c";
+  assume "M == norm_pres_extensions E p F f" "c : chain M" 
+         "(x, y) : Union c" " (x, z) : Union c";
   hence "EX H h. (x, y) : graph H h & (x, z) : graph H h"; 
   proof (elim UnionE chainE2); 
-    fix G1 G2; assume "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
+    fix G1 G2; 
+    assume "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
     have "G1 : M"; ..;
     hence e1: "EX H1 h1. graph H1 h1 = G1";  
       by (force! dest: norm_pres_extension_D);
@@ -225,11 +243,12 @@
   qed;
 qed;
 
-
-lemma sup_lf: "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c|] 
+lemma sup_lf: 
+  "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c|] 
    ==> is_linearform H h";
 proof -; 
-  assume "M = norm_pres_extensions E p F f" "c: chain M" "graph H h = Union c";
+  assume "M = norm_pres_extensions E p F f" "c: chain M"
+         "graph H h = Union c";
  
   let ?P = "%H h. is_linearform H h 
                     & is_subspace H E 
@@ -242,9 +261,10 @@
     fix x y; assume "x : H" "y : H"; 
     show "h (x [+] y) = h x + h y"; 
     proof -;
-      have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) &
-                    is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
-                    (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
+      have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) 
+                    & is_linearform H' h' & is_subspace H' E 
+                    & is_subspace F H' &  (graph F f <= graph H' h') 
+                    & (ALL x:H'. h' x <= p x)";
         by (rule some_H'h'2);
       thus ?thesis; 
       proof (elim exE conjE);
@@ -253,7 +273,8 @@
           and "is_linearform H' h'" "is_subspace H' E";
         have h'x: "h' x = h x"; ..;
         have h'y: "h' y = h y"; ..;
-        have h'xy: "h' (x [+] y) = h' x + h' y"; by (rule linearform_add_linear);
+        have h'xy: "h' (x [+] y) = h' x + h' y"; 
+          by (rule linearform_add_linear);
         have "h' (x [+] y) = h (x [+] y)";  
         proof -;
           have "x [+] y : H'"; ..;
@@ -263,14 +284,14 @@
           by (simp!); 
       qed;
     qed;
-
   next;  
     fix a x; assume  "x : H";
     show "h (a [*] x) = a * (h x)"; 
     proof -;
-      have "EX H' h'. x:H' & (graph H' h' <= graph H h) &
-                      is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
-                      (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)";
+      have "EX H' h'. x:H' & (graph H' h' <= graph H h) 
+                    & is_linearform H' h' & is_subspace H' E
+                    & is_subspace F H' & (graph F f <= graph H' h') 
+                    & (ALL x:H'. h' x <= p x)";
 	by (rule some_H'h');
       thus ?thesis; 
       proof (elim exE conjE);
@@ -278,7 +299,8 @@
 	assume b: "graph H' h' <= graph H h";
 	assume "x:H'" "is_linearform H' h'" "is_subspace H' E";
 	have h'x: "h' x = h x"; ..;
-	have h'ax: "h' (a [*] x) = a * h' x"; by (rule linearform_mult_linear);
+	have h'ax: "h' (a [*] x) = a * h' x"; 
+          by (rule linearform_mult_linear);
 	have "h' (a [*] x) = h (a [*] x)";
 	proof -;
 	  have "a [*] x : H'"; ..;
@@ -291,12 +313,13 @@
   qed;
 qed;
 
-
-lemma sup_ext: "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c|] 
-   ==> graph F f <= graph H h";
+lemma sup_ext:
+  "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; 
+  graph H h = Union c|] ==> graph F f <= graph H h";
 proof -;
-  assume "M = norm_pres_extensions E p F f" "c: chain M"  "graph H h = Union c"
-    and  e: "EX x. x:c";
+  assume "M = norm_pres_extensions E p F f" "c: chain M" 
+         "graph H h = Union c"
+  and e: "EX x. x:c";
  
   thus ?thesis; 
   proof (elim exE);
@@ -331,10 +354,12 @@
 qed;
 
 
-lemma sup_supF: "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c;
-                    is_subspace F E |] ==> is_subspace F H";
+lemma sup_supF: 
+  "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
+  graph H h = Union c; is_subspace F E |] ==> is_subspace F H";
 proof -; 
-  assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c" "graph H h = Union c"
+  assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c" 
+         "graph H h = Union c"
     "is_subspace F E";
 
   show ?thesis; 
@@ -359,11 +384,12 @@
 qed;
 
 
-lemma sup_subE: "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; graph H h = Union c;
-                    is_subspace F E|] ==> is_subspace H E";
+lemma sup_subE: 
+  "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; 
+  graph H h = Union c; is_subspace F E|] ==> is_subspace H E";
 proof -; 
-  assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c" "graph H h = Union c"
-    "is_subspace F E";
+  assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c" 
+         "graph H h = Union c" "is_subspace F E";
 
   show ?thesis; 
   proof;
@@ -380,9 +406,9 @@
       fix x; assume "x:H";
       show "x:E";
       proof -;
-	have "EX H' h'. x:H' & (graph H' h' <= graph H h) & 
-               is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
-               (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
+	have "EX H' h'. x:H' & (graph H' h' <= graph H h) 
+              & is_linearform H' h' & is_subspace H' E & is_subspace F H' 
+              & (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
 	  by (rule some_H'h');
 	thus ?thesis;
 	proof (elim exE conjE);
@@ -400,13 +426,15 @@
       fix x y; assume "x:H" "y:H";
       show "x [+] y : H";   
       proof -;
- 	have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) & 
-               is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
-               (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
+ 	have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) 
+              & is_linearform H' h' & is_subspace H' E & is_subspace F H'
+              & (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
 	  by (rule some_H'h'2); 
 	thus ?thesis;
 	proof (elim exE conjE); 
-	  fix H' h'; assume "x:H'" "y:H'" "is_subspace H' E" "graph H' h' <= graph H h";
+	  fix H' h'; 
+          assume "x:H'" "y:H'" "is_subspace H' E" 
+                 "graph H' h' <= graph H h";
 	  have "H' <= H"; ..;
 	  thus ?thesis;
 	  proof (rule subsetD);
@@ -427,7 +455,8 @@
 	  by (rule some_H'h'); 
 	thus ?thesis;
 	proof (elim exE conjE);
-	  fix H' h'; assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
+	  fix H' h'; 
+          assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
   	  have "H' <= H"; ..;
 	  thus ?thesis;
 	  proof (rule subsetD);
@@ -439,21 +468,22 @@
   qed;
 qed;
 
-
-lemma sup_norm_pres: "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c|] 
-   ==> ALL x::'a:H. h x <= p x";
+lemma sup_norm_pres: "[| M = norm_pres_extensions E p F f; c: chain M; 
+  graph H h = Union c|] ==> ALL x::'a:H. h x <= p x";
 proof;
-  assume "M = norm_pres_extensions E p F f" "c: chain M" "graph H h = Union c";
+  assume "M = norm_pres_extensions E p F f" "c: chain M" 
+         "graph H h = Union c";
   fix x; assume "x:H";
   show "h x <= p x"; 
   proof -; 
-    have "EX H' h'. x:H' & (graph H' h' <= graph H h) & 
-               is_linearform H' h' & is_subspace H' E & is_subspace F H' & 
-               (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
+    have "EX H' h'. x:H' & (graph H' h' <= graph H h) 
+                & is_linearform H' h' & is_subspace H' E & is_subspace F H'
+                & (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; 
       by (rule some_H'h');
     thus ?thesis; 
     proof (elim exE conjE);
-      fix H' h'; assume "x: H'" "graph H' h' <= graph H h" and a: "ALL x: H'. h' x <= p x" ;
+      fix H' h'; assume "x: H'" "graph H' h' <= graph H h" 
+      and a: "ALL x: H'. h' x <= p x" ;
       have "h x = h' x"; 
       proof (rule sym); 
         show "h' x = h x"; ..;
@@ -464,5 +494,4 @@
   qed;
 qed;
 
-
-end;
+end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/LinearSpace.thy
--- a/src/HOL/Real/HahnBanach/LinearSpace.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/LinearSpace.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,96 +3,107 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+header {* Linear Spaces *};
+
 theory LinearSpace = Bounds + Aux:;
 
-
-section {* vector spaces *};
+subsection {* Signature *};
 
 consts
-  sum	:: "['a, 'a] => 'a"                      (infixl "[+]" 65)  
-  prod  :: "[real, 'a] => 'a"                    (infixr "[*]" 70) 
-  zero  :: 'a                                    ("<0>");
+  sum	:: "['a, 'a] => 'a"                              (infixl "[+]" 65)
+  prod  :: "[real, 'a] => 'a"                            (infixr "[*]" 70) 
+  zero  :: 'a                                            ("<0>");
 
 constdefs
-  negate :: "'a => 'a"                           ("[-] _" [100] 100)
+  negate :: "'a => 'a"                                   ("[-] _" [100] 100)
   "[-] x == (- 1r) [*] x"
-  diff :: "'a => 'a => 'a"                       (infixl "[-]" 68)
+  diff :: "'a => 'a => 'a"                               (infixl "[-]" 68)
   "x [-] y == x [+] [-] y";
 
+subsection {* Vector space laws *}
+(***
 constdefs
   is_vectorspace :: "'a set => bool"
-  "is_vectorspace V == <0>:V &
-   (ALL x:V. ALL y:V. ALL z:V. ALL a b. x [+] y: V 
-                          & a [*] x: V                        
-                          & x [+] y [+] z = x [+] (y [+] z)  
-                          & x [+] y = y [+] x             
-                          & x [-] x = <0>         
-                          & <0> [+] x = x 
-                          & a [*] (x [+] y) = a [*] x [+] a [*] y
-                          & (a + b) [*] x = a [*] x [+] b [*] x
-                          & (a * b) [*] x = a [*] b [*] x     
-                          & 1r [*] x = x)";
-
-
-subsection {* neg, diff *};
-
-lemma vs_mult_minus_1: "(- 1r) [*] x = [-] x";
-  by (simp add: negate_def);
-
-lemma vs_add_mult_minus_1_eq_diff: "x [+] (- 1r) [*] y = x [-] y";
-  by (simp add: diff_def negate_def);
-
-lemma vs_add_minus_eq_diff: "x [+] [-] y = x [-] y";
-  by (simp add: diff_def);
+  "is_vectorspace V == V ~= {} 
+   & (ALL x: V. ALL a. a [*] x: V)
+   & (ALL x: V. ALL y: V. x [+] y = y [+] x)
+   & (ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z =  x [+] (y [+] z))
+   & (ALL x: V. ALL y: V. x [+] y: V)
+   & (ALL x: V. x [-] x = <0>)
+   & (ALL x: V. <0> [+] x = x)
+   & (ALL x: V. ALL y: V. ALL a. a [*] (x [+] y) = a [*] x [+] a [*] y)
+   & (ALL x: V. ALL a b. (a + b) [*] x = a [*] x [+] b [*] x)
+   & (ALL x: V. ALL a b. (a * b) [*] x = a [*] b [*] x)
+   & (ALL x: V. 1r [*] x = x)"; 
+***)
+constdefs
+  is_vectorspace :: "'a set => bool"
+  "is_vectorspace V == V ~= {} 
+   & (ALL x:V. ALL y:V. ALL z:V. ALL a b. 
+        x [+] y: V 
+      & a [*] x: V                         
+      & x [+] y [+] z = x [+] (y [+] z)  
+      & x [+] y = y [+] x             
+      & x [-] x = <0>         
+      & <0> [+] x = x 
+      & a [*] (x [+] y) = a [*] x [+] a [*] y
+      & (a + b) [*] x = a [*] x [+] b [*] x
+      & (a * b) [*] x = a [*] b [*] x     
+      & 1r [*] x = x)";
 
 lemma vsI [intro]:
   "[| <0>:V; \
-  \      ALL x: V. ALL a::real. a [*] x: V; \     
-  \      ALL x: V. ALL y: V. x [+] y = y [+] x; \
-  \      ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z =  x [+] (y [+] z); \
-  \      ALL x: V. ALL y: V. x [+] y: V; \
-  \      ALL x: V.  x [-] x = <0>; \
-  \      ALL x: V.  <0> [+] x = x; \
-  \      ALL x: V. ALL y: V. ALL a::real. a [*] (x [+] y) = a [*] x [+] a [*] y; \
-  \      ALL x: V. ALL a::real. ALL b::real. (a + b) [*] x = a [*] x [+] b [*] x; \
-  \      ALL x: V. ALL a::real. ALL b::real. (a * b) [*] x = a [*] b [*] x; \
-  \      ALL x: V. 1r [*] x = x |] ==> is_vectorspace V";
+       ALL x: V. ALL y: V. x [+] y: V;
+       ALL x: V. ALL a. a [*] x: V;    
+       ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z =  x [+] (y [+] z);
+       ALL x: V. ALL y: V. x [+] y = y [+] x;
+       ALL x: V. x [-] x = <0>;
+       ALL x: V. <0> [+] x = x;
+       ALL x: V. ALL y: V. ALL a. a [*] (x [+] y) = a [*] x [+] a [*] y;
+       ALL x: V. ALL a b. (a + b) [*] x = a [*] x [+] b [*] x;
+       ALL x: V. ALL a b. (a * b) [*] x = a [*] b [*] x; \
+       ALL x: V. 1r [*] x = x |] ==> is_vectorspace V";
 proof (unfold is_vectorspace_def, intro conjI ballI allI);
   fix x y z; assume "x:V" "y:V" "z:V"; 
   assume "ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z =  x [+] (y [+] z)";
   thus "x [+] y [+] z =  x [+] (y [+] z)"; by (elim bspec[elimify]);
 qed force+;
 
-lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
+lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})"; 
+  by (unfold is_vectorspace_def) simp;
+ 
+lemma vs_add_closed [simp, intro!!]: 
+  "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V"; 
   by (unfold is_vectorspace_def) simp;
 
-lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})"; 
-  by (unfold is_vectorspace_def) fast;
- 
-lemma vs_add_closed [simp, intro!!]: "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V"; 
+lemma vs_mult_closed [simp, intro!!]: 
+  "[| is_vectorspace V; x: V |] ==> a [*] x: V"; 
   by (unfold is_vectorspace_def) simp;
 
-lemma vs_mult_closed [simp, intro!!]: "[| is_vectorspace V; x: V |] ==> a [*] x: V"; 
-  by (unfold is_vectorspace_def) simp;
-
-lemma vs_diff_closed [simp, intro!!]: "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
+lemma vs_diff_closed [simp, intro!!]: 
+ "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
   by (unfold diff_def negate_def) simp;
 
-lemma vs_neg_closed  [simp, intro!!]: "[| is_vectorspace V; x: V |] ==>  [-] x: V";
+lemma vs_neg_closed  [simp, intro!!]: 
+  "[| is_vectorspace V; x: V |] ==>  [-] x: V";
   by (unfold negate_def) simp;
 
 lemma vs_add_assoc [simp]:  
-  "[| is_vectorspace V; x: V; y: V; z: V|] ==> x [+] y [+] z =  x [+] (y [+] z)";
+  "[| is_vectorspace V; x: V; y: V; z: V|]
+   ==> x [+] y [+] z = x [+] (y [+] z)";
   by (unfold is_vectorspace_def) fast;
 
-lemma vs_add_commute [simp]: "[| is_vectorspace V; x:V; y:V |] ==> y [+] x = x [+] y";
+lemma vs_add_commute [simp]: 
+  "[| is_vectorspace V; x:V; y:V |] ==> y [+] x = x [+] y";
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_add_left_commute [simp]:
-  "[| is_vectorspace V; x:V; y:V; z:V |] ==> x [+] (y [+] z) = y [+] (x [+] z)";
+  "[| is_vectorspace V; x:V; y:V; z:V |] 
+  ==> x [+] (y [+] z) = y [+] (x [+] z)";
 proof -;
   assume "is_vectorspace V" "x:V" "y:V" "z:V";
-  hence "x [+] (y [+] z) = (x [+] y) [+] z"; by (simp only: vs_add_assoc);
+  hence "x [+] (y [+] z) = (x [+] y) [+] z"; 
+    by (simp only: vs_add_assoc);
   also; have "... = (y [+] x) [+] z"; by (simp! only: vs_add_commute);
   also; have "... = y [+] (x [+] z)"; by (simp! only: vs_add_assoc);
   finally; show ?thesis; .;
@@ -100,13 +111,30 @@
 
 theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
 
-lemma vs_diff_self [simp]: "[| is_vectorspace V; x:V |] ==>  x [-] x = <0>"; 
+lemma vs_diff_self [simp]: 
+  "[| is_vectorspace V; x:V |] ==>  x [-] x = <0>"; 
   by (unfold is_vectorspace_def) simp;
 
-lemma vs_add_zero_left [simp]: "[| is_vectorspace V; x:V |] ==>  <0> [+] x = x";
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
+proof -; 
+  assume "is_vectorspace V";
+  have "V ~= {}"; ..;
+  hence "EX x. x:V"; by force;
+  thus ?thesis; 
+  proof; 
+    fix x; assume "x:V"; 
+    have "<0> = x [-] x"; by (simp!);
+    also; have "... : V"; by (simp! only: vs_diff_closed);
+    finally; show ?thesis; .;
+  qed;
+qed;
+
+lemma vs_add_zero_left [simp]: 
+  "[| is_vectorspace V; x:V |] ==>  <0> [+] x = x";
   by (unfold is_vectorspace_def) simp;
 
-lemma vs_add_zero_right [simp]: "[| is_vectorspace V; x:V |] ==>  x [+] <0> = x";
+lemma vs_add_zero_right [simp]: 
+  "[| is_vectorspace V; x:V |] ==>  x [+] <0> = x";
 proof -;
   assume "is_vectorspace V" "x:V";
   hence "x [+] <0> = <0> [+] x"; by simp;
@@ -115,53 +143,67 @@
 qed;
 
 lemma vs_add_mult_distrib1: 
-  "[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [+] y) = a [*] x [+] a [*] y";
+  "[| is_vectorspace V; x:V; y:V |] 
+  ==> a [*] (x [+] y) = a [*] x [+] a [*] y";
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_add_mult_distrib2: 
-  "[| is_vectorspace V; x:V |] ==>  (a + b) [*] x = a [*] x [+] b [*] x"; 
+  "[| is_vectorspace V; x:V |] ==> (a + b) [*] x = a [*] x [+] b [*] x"; 
+  by (unfold is_vectorspace_def) simp;
+
+lemma vs_mult_assoc: 
+  "[| is_vectorspace V; x:V |] ==> (a * b) [*] x = a [*] (b [*] x)";   
   by (unfold is_vectorspace_def) simp;
 
-lemma vs_mult_assoc: "[| is_vectorspace V; x:V |] ==> (a * b) [*] x = a [*] (b [*] x)";   
-  by (unfold is_vectorspace_def) simp;
-
-lemma vs_mult_assoc2 [simp]: "[| is_vectorspace V; x:V |] ==> a [*] b [*] x = (a * b) [*] x";
+lemma vs_mult_assoc2 [simp]: 
+ "[| is_vectorspace V; x:V |] ==> a [*] b [*] x = (a * b) [*] x";
   by (simp only: vs_mult_assoc);
 
-lemma vs_mult_1 [simp]: "[| is_vectorspace V; x:V |] ==> 1r [*] x = x"; 
+lemma vs_mult_1 [simp]: 
+  "[| is_vectorspace V; x:V |] ==> 1r [*] x = x"; 
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_diff_mult_distrib1: 
-  "[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [-] y) = a [*] x [-] a [*] y";
+  "[| is_vectorspace V; x:V; y:V |] 
+  ==> a [*] (x [-] y) = a [*] x [-] a [*] y";
   by (simp add: diff_def negate_def vs_add_mult_distrib1);
 
-lemma vs_minus_eq: "[| is_vectorspace V; x:V |] ==> - b [*] x = [-] (b [*] x)";
+lemma vs_minus_eq: "[| is_vectorspace V; x:V |] 
+  ==> - b [*] x = [-] (b [*] x)";
   by (simp add: negate_def);
 
 lemma vs_diff_mult_distrib2: 
-  "[| is_vectorspace V; x:V |] ==> (a - b) [*] x = a [*] x [-] (b [*] x)";
+  "[| is_vectorspace V; x:V |] 
+  ==> (a - b) [*] x = a [*] x [-] (b [*] x)";
 proof -;
   assume "is_vectorspace V" "x:V";
-  have " (a - b) [*] x = (a + - b ) [*] x"; by (unfold real_diff_def, simp);
-  also; have "... = a [*] x [+] (- b) [*] x"; by (rule vs_add_mult_distrib2);
-  also; have "... = a [*] x [+] [-] (b [*] x)"; by (simp! add: vs_minus_eq);
+  have " (a - b) [*] x = (a + - b ) [*] x"; 
+    by (unfold real_diff_def, simp);
+  also; have "... = a [*] x [+] (- b) [*] x"; 
+    by (rule vs_add_mult_distrib2);
+  also; have "... = a [*] x [+] [-] (b [*] x)"; 
+    by (simp! add: vs_minus_eq);
   also; have "... = a [*] x [-] (b [*] x)"; by (unfold diff_def, simp);
   finally; show ?thesis; .;
 qed;
 
-lemma vs_mult_zero_left [simp]: "[| is_vectorspace V; x: V|] ==> 0r [*] x = <0>";
+lemma vs_mult_zero_left [simp]: 
+  "[| is_vectorspace V; x: V|] ==> 0r [*] x = <0>";
 proof -;
   assume "is_vectorspace V" "x:V";
   have  "0r [*] x = (1r - 1r) [*] x"; by (simp only: real_diff_self);
   also; have "... = (1r + - 1r) [*] x"; by simp;
-  also; have "... =  1r [*] x [+] (- 1r) [*] x"; by (rule vs_add_mult_distrib2);
+  also; have "... =  1r [*] x [+] (- 1r) [*] x"; 
+    by (rule vs_add_mult_distrib2);
   also; have "... = x [+] (- 1r) [*] x"; by (simp!);
-  also; have "... = x [-] x"; by (rule vs_add_mult_minus_1_eq_diff);
+  also; have "... = x [+] [-] x"; by (fold negate_def) simp;
+  also; have "... = x [-] x"; by (fold diff_def) simp;
   also; have "... = <0>"; by (simp!);
   finally; show ?thesis; .;
 qed;
 
-lemma vs_mult_zero_right [simp]: "[| is_vectorspace (V:: 'a set) |] ==> a [*] <0> = (<0>::'a)";
+lemma vs_mult_zero_right [simp]: 
+  "[| is_vectorspace (V:: 'a set) |] ==> a [*] <0> = (<0>::'a)";
 proof -;
   assume "is_vectorspace V";
   have "a [*] <0> = a [*] (<0> [-] (<0>::'a))"; by (simp!);
@@ -171,38 +213,46 @@
   finally; show ?thesis; .;
 qed;
 
-lemma vs_minus_mult_cancel [simp]:  "[| is_vectorspace V; x:V |] ==>  (- a) [*] [-] x = a [*] x";
+lemma vs_minus_mult_cancel [simp]:  
+  "[| is_vectorspace V; x:V |] ==> (- a) [*] [-] x = a [*] x";
   by (unfold negate_def) simp;
 
-lemma vs_add_minus_left_eq_diff: "[| is_vectorspace V; x:V; y:V |] ==>  [-] x [+] y = y [-] x";
+lemma vs_add_minus_left_eq_diff: 
+  "[| is_vectorspace V; x:V; y:V |] ==> [-] x [+] y = y [-] x";
 proof -; 
   assume "is_vectorspace V" "x:V" "y:V";
-  have "[-] x [+] y = y [+] [-] x"; by (simp! add: vs_add_commute [RS sym, of V "[-] x"]);
-  also; have "... = y [-] x"; by (simp! only: vs_add_minus_eq_diff);
+  have "[-] x [+] y = y [+] [-] x"; 
+    by (simp! add: vs_add_commute [RS sym, of V "[-] x"]);
+  also; have "... = y [-] x"; by (unfold diff_def) simp;
   finally; show ?thesis; .;
 qed;
 
-lemma vs_add_minus [simp]: "[| is_vectorspace V; x:V|] ==> x [+] [-] x = <0>";
-  by (simp add: vs_add_minus_eq_diff); 
+lemma vs_add_minus [simp]: 
+  "[| is_vectorspace V; x:V|] ==> x [+] [-] x = <0>";
+  by (fold diff_def) simp;
 
-lemma vs_add_minus_left [simp]: "[| is_vectorspace V; x:V |] ==> [-] x [+]  x = <0>";
-  by (simp add: vs_add_minus_eq_diff); 
+lemma vs_add_minus_left [simp]: 
+  "[| is_vectorspace V; x:V |] ==> [-] x [+]  x = <0>";
+  by (fold diff_def) simp;
 
-lemma vs_minus_minus [simp]: "[| is_vectorspace V; x:V|] ==> [-] [-] x = x";
+lemma vs_minus_minus [simp]: 
+  "[| is_vectorspace V; x:V|] ==> [-] [-] x = x";
   by (unfold negate_def) simp;
 
-lemma vs_minus_zero [simp]: "[| is_vectorspace (V::'a set)|] ==>  [-] (<0>::'a) = <0>"; 
+lemma vs_minus_zero [simp]: 
+  "[| is_vectorspace (V::'a set)|] ==> [-] (<0>::'a) = <0>"; 
   by (unfold negate_def) simp;
 
 lemma vs_minus_zero_iff [simp]:
-  "[| is_vectorspace V; x:V|] ==>  ([-] x = <0>) = (x = <0>)" (concl is "?L = ?R");
+  "[| is_vectorspace V; x:V|] ==> ([-] x = <0>) = (x = <0>)" 
+  (concl is "?L = ?R");
 proof -;
   assume vs: "is_vectorspace V" "x:V";
   show "?L = ?R";
   proof;
     assume l: ?L;
     have "x = [-] [-] x"; by (rule vs_minus_minus [RS sym]);
-    also; have "... = [-] <0>"; by (rule l [RS arg_cong] );
+    also; have "... = [-] <0>"; by (simp only: l);
     also; have "... = <0>"; by (rule vs_minus_zero);
     finally; show ?R; .;
   next;
@@ -211,33 +261,41 @@
   qed;
 qed;
 
-lemma vs_add_minus_cancel [simp]:  "[| is_vectorspace V; x:V; y:V|] ==>  x [+] ([-] x [+] y) = y"; 
+lemma vs_add_minus_cancel [simp]:  
+  "[| is_vectorspace V; x:V; y:V|] ==>  x [+] ([-] x [+] y) = y"; 
   by (simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
 
-lemma vs_minus_add_cancel [simp]: "[| is_vectorspace V; x:V; y:V |] ==>  [-] x [+] (x [+] y) = y"; 
+lemma vs_minus_add_cancel [simp]: 
+  "[| is_vectorspace V; x:V; y:V |] ==>  [-] x [+] (x [+] y) = y"; 
   by (simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
 
 lemma vs_minus_add_distrib [simp]:  
-  "[| is_vectorspace V; x:V; y:V|] ==>  [-] (x [+] y) = [-] x [+] [-] y";
+  "[| is_vectorspace V; x:V; y:V|] 
+  ==> [-] (x [+] y) = [-] x [+] [-] y";
   by (unfold negate_def, simp add: vs_add_mult_distrib1);
 
-lemma vs_diff_zero [simp]: "[| is_vectorspace V; x:V |] ==> x [-] <0> = x";
+lemma vs_diff_zero [simp]: 
+  "[| is_vectorspace V; x:V |] ==> x [-] <0> = x";
   by (unfold diff_def) simp;  
 
-lemma vs_diff_zero_right [simp]: "[| is_vectorspace V; x:V |] ==> <0> [-] x = [-] x";
+lemma vs_diff_zero_right [simp]: 
+  "[| is_vectorspace V; x:V |] ==> <0> [-] x = [-] x";
   by (unfold diff_def) simp;
 
 lemma vs_add_left_cancel:
-  "[|is_vectorspace V; x:V; y:V; z:V|] ==> (x [+] y = x [+] z) = (y = z)"  
+  "[| is_vectorspace V; x:V; y:V; z:V|] 
+   ==> (x [+] y = x [+] z) = (y = z)"  
   (concl is "?L = ?R");
 proof;
   assume "is_vectorspace V" "x:V" "y:V" "z:V";
   assume l: ?L; 
   have "y = <0> [+] y"; by (simp!);
   also; have "... = [-] x [+] x [+] y"; by (simp!);
-  also; have "... = [-] x [+] (x [+] y)"; by (simp! only: vs_add_assoc vs_neg_closed);
+  also; have "... = [-] x [+] (x [+] y)"; 
+    by (simp! only: vs_add_assoc vs_neg_closed);
   also; have "...  = [-] x [+] (x [+] z)"; by (simp only: l);
-  also; have "... = [-] x [+] x [+] z"; by (rule vs_add_assoc [RS sym]) (simp!)+;
+  also; have "... = [-] x [+] x [+] z"; 
+    by (rule vs_add_assoc [RS sym]) (simp!)+;
   also; have "... = z"; by (simp!);
   finally; show ?R;.;
 next;    
@@ -246,15 +304,18 @@
 qed;
 
 lemma vs_add_right_cancel: 
-  "[| is_vectorspace V; x:V; y:V; z:V |] ==>  (y [+] x = z [+] x) = (y = z)";  
+  "[| is_vectorspace V; x:V; y:V; z:V |] 
+  ==> (y [+] x = z [+] x) = (y = z)";  
   by (simp only: vs_add_commute vs_add_left_cancel);
 
-lemma vs_add_assoc_cong [tag FIXME simp]: "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |] 
+lemma vs_add_assoc_cong [tag FIXME simp]: 
+  "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |] 
   ==> x [+] y = x' [+] y' ==> x [+] (y [+] z) = x' [+] (y' [+] z)"; 
-  by (simp del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
+  by (simp del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]); 
 
 lemma vs_mult_left_commute: 
-  "[| is_vectorspace V; x:V; y:V; z:V |] ==>  x [*] y [*] z = y [*] x [*] z";  
+  "[| is_vectorspace V; x:V; y:V; z:V |] 
+  ==> x [*] y [*] z = y [*] x [*] z";  
   by (simp add: real_mult_commute);
 
 lemma vs_mult_zero_uniq :
@@ -271,14 +332,16 @@
 qed;
 
 lemma vs_mult_left_cancel: 
-  "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==>  (a [*] x = a [*] y) = (x = y)"
+  "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==> 
+  (a [*] x = a [*] y) = (x = y)"
   (concl is "?L = ?R");
 proof;
   assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";
   assume l: ?L;
   have "x = 1r [*] x"; by (simp!);
   also; have "... = (rinv a * a) [*] x"; by (simp!);
-  also; have "... = rinv a [*] (a [*] x)"; by (simp! only: vs_mult_assoc);
+  also; have "... = rinv a [*] (a [*] x)"; 
+    by (simp! only: vs_mult_assoc);
   also; have "... = rinv a [*] (a [*] y)"; by (simp only: l);
   also; have "... = y"; by (simp!);
   finally; show ?R;.;
@@ -287,12 +350,27 @@
   thus ?L; by simp;
 qed;
 
+lemma vs_mult_right_cancel: (*** forward ***)
+  "[| is_vectorspace V; x:V; x ~= <0> |] ==>  (a [*] x = b [*] x) = (a = b)"
+  (concl is "?L = ?R");
+proof;
+  assume "is_vectorspace V" "x:V" "x ~= <0>";
+  assume l: ?L;
+  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; have "(a - b) [*] x  = <0>"; .; 
+  hence "a - b = 0r"; by (simp! add:  vs_mult_zero_uniq);
+  thus "a = b"; by (rule real_add_minus_eq);
+next;
+  assume ?R;
+  thus ?L; by simp;
+qed; (*** backward :
 lemma vs_mult_right_cancel: 
   "[| is_vectorspace V; x:V; x ~= <0> |] ==>  (a [*] x = b [*] x) = (a = b)"
   (concl is "?L = ?R");
 proof;
   assume "is_vectorspace V" "x:V" "x ~= <0>";
-  assume l: ?L;
+  assume l: ?L; 
   show "a = b"; 
   proof (rule real_add_minus_eq);
     show "a - b = 0r"; 
@@ -306,9 +384,11 @@
   assume ?R;
   thus ?L; by simp;
 qed;
+**)
 
 lemma vs_eq_diff_eq: 
-  "[| is_vectorspace V; x:V; y:V; z:V |] ==>  (x = z [-] y) = (x [+] y = z)"
+  "[| is_vectorspace V; x:V; y:V; z:V |] ==> 
+  (x = z [-] y) = (x [+] y = z)"
    (concl is "?L = ?R" );  
 proof -;
   assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
@@ -316,60 +396,74 @@
   proof;
     assume l: ?L;
     have "x [+] y = z [-] y [+] y"; by (simp add: l);
-    also; have "... = z [+] [-] y [+] y"; by (simp only: vs_add_minus_eq_diff);
-    also; have "... = z [+] ([-] y [+] y)"; by (rule vs_add_assoc) (simp!)+;
-    also; from vs; have "... = z [+] <0>"; by (simp only: vs_add_minus_left);
+    also; have "... = z [+] [-] y [+] y"; by (unfold diff_def) simp;
+    also; have "... = z [+] ([-] y [+] y)"; 
+      by (rule vs_add_assoc) (simp!)+;
+    also; from vs; have "... = z [+] <0>"; 
+      by (simp only: vs_add_minus_left);
     also; from vs; have "... = z"; by (simp only: vs_add_zero_right);
     finally; show ?R;.;
   next;
     assume r: ?R;
     have "z [-] y = (x [+] y) [-] y"; by (simp only: r);
-    also; from vs; have "... = x [+] y [+] [-] y"; by (simp only: vs_add_minus_eq_diff);
-    also; have "... = x [+] (y [+] [-] y)"; by (rule vs_add_assoc) (simp!)+;
+    also; from vs; have "... = x [+] y [+] [-] y"; 
+      by (unfold diff_def) simp;
+    also; have "... = x [+] (y [+] [-] y)"; 
+      by (rule vs_add_assoc) (simp!)+;
     also; have "... = x"; by (simp!);
     finally; show ?L; by (rule sym);
   qed;
 qed;
 
-lemma vs_add_minus_eq_minus: "[| is_vectorspace V; x:V; y:V; <0> = x [+] y|] ==> y = [-] x"; 
+lemma vs_add_minus_eq_minus: 
+  "[| is_vectorspace V; x:V; y:V; <0> = x [+] y|] ==> y = [-] x"; 
 proof -;
   assume vs: "is_vectorspace V" "x:V" "y:V"; 
   assume "<0> = x [+] y";
   have "[-] x = [-] x [+] <0>"; by (simp!);
   also; have "... = [-] x [+] (x [+] y)";  by (simp!);
-  also; have "... = [-] x [+] x [+] y"; by (rule vs_add_assoc [RS sym]) (simp!)+;
+  also; have "... = [-] x [+] x [+] y"; 
+    by (rule vs_add_assoc [RS sym]) (simp!)+;
   also; have "... = (x [+] [-] x) [+] y"; by (simp!);
   also; have "... = y"; by (simp!);
   finally; show ?thesis; by (rule sym);
 qed;  
 
-lemma vs_add_minus_eq: "[| is_vectorspace V; x:V; y:V; x [-] y = <0> |] ==> x = y"; 
+lemma vs_add_minus_eq: 
+  "[| is_vectorspace V; x:V; y:V; x [-] y = <0> |] ==> x = y"; 
 proof -;
   assume "is_vectorspace V" "x:V" "y:V" "x [-] y = <0>";
   have "x [+] [-] y = x [-] y"; by (unfold diff_def, simp);
   also; have "... = <0>"; .;
   finally; have e: "<0> = x [+] [-] y"; by (rule sym);
   have "x = [-] [-] x"; by (simp!);
-  also; have "[-] x = [-] y"; by (rule vs_add_minus_eq_minus [RS sym]) (simp! add: e)+;
+  also; have "[-] x = [-] y"; 
+    by (rule vs_add_minus_eq_minus [RS sym]) (simp! add: e)+;
   also; have "[-] ... = y"; by (simp!); 
   finally; show "x = y"; .;
 qed;
 
 lemma vs_add_diff_swap:
-  "[| is_vectorspace V; a:V; b:V; c:V; d:V; a [+] b = c [+] d|] ==> a [-] c = d [-] b";
+  "[| is_vectorspace V; a:V; b:V; c:V; d:V; a [+] b = c [+] d|] 
+  ==> a [-] c = d [-] b";
 proof -; 
-  assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" and eq: "a [+] b = c [+] d";
-  have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; by (simp! add: vs_add_left_cancel);
+  assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" 
+  and eq: "a [+] b = c [+] d";
+  have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; 
+    by (simp! add: vs_add_left_cancel);
   also; have "... = d"; by (rule vs_minus_add_cancel);
   finally; have eq: "[-] c [+] (a [+] b) = d"; .;
-  from vs; have "a [-] c = ([-] c [+] (a [+] b)) [+] [-] b"; by (simp add: vs_add_ac diff_def);
-  also; from eq; have "...  = d [+] [-] b"; by (simp! add: vs_add_right_cancel);
+  from vs; have "a [-] c = ([-] c [+] (a [+] b)) [+] [-] b"; 
+    by (simp add: vs_add_ac diff_def);
+  also; from eq; have "...  = d [+] [-] b"; 
+    by (simp! add: vs_add_right_cancel);
   also; have "... = d [-] b"; by (simp add : diff_def);
   finally; show "a [-] c = d [-] b"; .;
 qed;
 
 lemma vs_add_cancel_21: 
-  "[| is_vectorspace V; x:V; y:V; z:V; u:V|] ==> (x [+] (y [+] z) = y [+] u) = ((x [+] z) = u)"
+  "[| is_vectorspace V; x:V; y:V; z:V; u:V|] 
+  ==> (x [+] (y [+] z) = y [+] u) = ((x [+] z) = u)"
   (concl is "?L = ?R" ); 
 proof -; 
   assume vs: "is_vectorspace V" "x:V" "y:V""z:V" "u:V";
@@ -378,22 +472,26 @@
     assume l: ?L;
     have "u = <0> [+] u"; by (simp!);
     also; have "... = [-] y [+] y [+] u"; by (simp!);
-    also; have "... = [-] y [+] (y [+] u)"; by (rule vs_add_assoc) (simp!)+;
+    also; have "... = [-] y [+] (y [+] u)"; 
+      by (rule vs_add_assoc) (simp!)+;
     also; have "... = [-] y [+] (x [+] (y [+] z))"; by (simp only: l);
     also; have "... = [-] y [+] (y [+] (x [+] z))"; by (simp!);
-    also; have "... = [-] y [+] y [+] (x [+] z)"; by (rule vs_add_assoc [RS sym]) (simp!)+;
+    also; have "... = [-] y [+] y [+] (x [+] z)"; 
+      by (rule vs_add_assoc [RS sym]) (simp!)+;
     also; have "... = (x [+] z)"; by (simp!);
     finally; show ?R; by (rule sym);
   next;
     assume r: ?R;
-    have "x [+] (y [+] z) = y [+] (x [+] z)"; by (simp! only: vs_add_left_commute [of V x]);
+    have "x [+] (y [+] z) = y [+] (x [+] z)"; 
+      by (simp! only: vs_add_left_commute [of V x]);
     also; have "... = y [+] u"; by (simp only: r);
     finally; show ?L; .;
   qed;
 qed;
 
 lemma vs_add_cancel_end: 
-  "[| is_vectorspace V;  x:V; y:V; z:V |] ==> (x [+] (y [+] z) = y) = (x = [-] z)"
+  "[| is_vectorspace V;  x:V; y:V; z:V |] 
+  ==> (x [+] (y [+] z) = y) = (x = [-] z)"
   (concl is "?L = ?R" );
 proof -;
   assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
@@ -404,7 +502,8 @@
     proof (rule vs_add_left_cancel [RS iffD1]);
       have "y [+] <0> = y"; by (simp! only: vs_add_zero_right); 
       also; have "... =  x [+] (y [+] z)"; by (simp only: l); 
-      also; have "... = y [+] (x [+] z)"; by (simp! only: vs_add_left_commute); 
+      also; have "... = y [+] (x [+] z)"; 
+        by (simp! only: vs_add_left_commute); 
       finally; show "y [+] <0> = y [+] (x [+] z)"; .;
   qed (simp!)+;
     hence "z = [-] x"; by (simp! only: vs_add_minus_eq_minus);
@@ -412,7 +511,8 @@
   next;
     assume r: ?R;
     have "x [+] (y [+] z) = [-] z [+] (y [+] z)"; by (simp only: r); 
-    also; have "... = y [+] ([-] z [+] z)"; by (simp! only: vs_add_left_commute);
+    also; have "... = y [+] ([-] z [+] z)"; 
+      by (simp! only: vs_add_left_commute);
     also; have "... = y [+] <0>";  by (simp!);
     also; have "... = y";  by (simp!);
     finally; show ?L; .;
@@ -422,5 +522,4 @@
 lemma it: "[| x = y; x' = y'|] ==> x [+] x' = y [+] y'";
   by simp; 
 
-
 end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,9 +3,9 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-theory Linearform = LinearSpace:;
+header {* Linearforms *};
 
-section {* linearforms *};
+theory Linearform = LinearSpace:;
 
 constdefs
   is_linearform :: "['a set, 'a => real] => bool" 
@@ -13,7 +13,8 @@
       (ALL x: V. ALL y: V. f (x [+] y) = f x + f y) &
       (ALL x: V. ALL a. f (a [*] x) = a * (f x))"; 
 
-lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
+lemma is_linearformI [intro]: 
+  "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
     !! x c. x : V ==> f (c [*] x) = c * f x |]
  ==> is_linearform V f";
  by (unfold is_linearform_def) force;
@@ -30,30 +31,33 @@
   "[|  is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";
 proof -; 
   assume "is_linearform V f" "is_vectorspace V" "x:V"; 
-  have "f ([-] x) = f ((- 1r) [*] x)"; by (simp! add: vs_mult_minus_1);
+  have "f ([-] x) = f ((- 1r) [*] x)"; by (unfold negate_def) simp;
   also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
   also; have "... = - (f x)"; by (simp!);
   finally; show ?thesis; .;
 qed;
 
 lemma linearform_diff_linear [intro!!]: 
-  "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y";  
+  "[| is_vectorspace V; is_linearform V f; x:V; y:V |] 
+  ==> f (x [-] y) = f x - f y";  
 proof -;
   assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
   have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def);
-  also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (simp!)+;
+  also; have "... = f x + f ([-] y)"; 
+    by (rule linearform_add_linear) (simp!)+;
   also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear);
   finally; show "f (x [-] y) = f x - f y"; by (simp!);
 qed;
 
-lemma linearform_zero [intro!!, simp]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
+lemma linearform_zero [intro!!, simp]: 
+  "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
 proof -; 
   assume "is_vectorspace V" "is_linearform V f";
   have "f <0> = f (<0> [-] <0>)"; by (simp!);
-  also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) (simp!)+;
+  also; have "... = f <0> - f <0>"; 
+    by (rule linearform_diff_linear) (simp!)+;
   also; have "... = 0r"; by simp;
   finally; show "f <0> = 0r"; .;
 qed; 
 
-end;
-
+end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,12 +3,14 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+header {* Normed vector spaces *};
+
 theory NormedSpace =  Subspace:;
 
 
-section {* normed vector spaces *};
 
-subsection {* quasinorm *};
+subsection {* Quasinorms *};
+
 
 constdefs
   is_quasinorm :: "['a set,  'a => real] => bool"
@@ -17,7 +19,7 @@
       & norm (a [*] x) = (rabs a) * (norm x)
       & norm (x [+] y) <= norm x + norm y";
 
-lemma is_quasinormI[intro]: 
+lemma is_quasinormI [intro]: 
   "[| !! x y a. [| x:V; y:V|] ==>  0r <= norm x;
       !! x a. x:V ==> norm (a [*] x) = (rabs a) * (norm x);
       !! x y. [|x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y |] 
@@ -29,36 +31,46 @@
   by (unfold is_quasinorm_def, force);
 
 lemma quasinorm_mult_distrib: 
-  "[| is_quasinorm V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
+  "[| is_quasinorm V norm; x:V |] 
+  ==> norm (a [*] x) = (rabs a) * (norm x)";
   by (unfold is_quasinorm_def, force);
 
 lemma quasinorm_triangle_ineq: 
-  "[| is_quasinorm V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
+  "[| is_quasinorm V norm; x:V; y:V |] 
+  ==> norm (x [+] y) <= norm x + norm y";
   by (unfold is_quasinorm_def, force);
 
 lemma quasinorm_diff_triangle_ineq: 
-  "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |] ==> norm (x [-] y) <= norm x + norm y";
+  "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |] 
+  ==> norm (x [-] y) <= norm x + norm y";
 proof -;
   assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V";
-  have "norm (x [-] y) = norm (x [+] - 1r [*] y)";  by (simp add: diff_def negate_def);
-  also; have "... <= norm x + norm  (- 1r [*] y)"; by (simp! add: quasinorm_triangle_ineq);
-  also; have "norm (- 1r [*] y) = rabs (- 1r) * norm y"; by (rule quasinorm_mult_distrib);
+  have "norm (x [-] y) = norm (x [+] - 1r [*] y)";  
+    by (simp add: diff_def negate_def);
+  also; have "... <= norm x + norm  (- 1r [*] y)"; 
+    by (simp! add: quasinorm_triangle_ineq);
+  also; have "norm (- 1r [*] y) = rabs (- 1r) * norm y"; 
+    by (rule quasinorm_mult_distrib);
   also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
   finally; show "norm (x [-] y) <= norm x + norm y"; by simp;
 qed;
 
 lemma quasinorm_minus: 
-  "[| is_quasinorm V norm; x:V; is_vectorspace V |] ==> norm ([-] x) = norm x";
+  "[| is_quasinorm V norm; x:V; is_vectorspace V |] 
+  ==> norm ([-] x) = norm x";
 proof -;
   assume "is_quasinorm V norm" "x:V" "is_vectorspace V";
   have "norm ([-] x) = norm (-1r [*] x)"; by (unfold negate_def) force;
-  also; have "... = rabs (-1r) * norm x"; by (rule quasinorm_mult_distrib);
+  also; have "... = rabs (-1r) * norm x"; 
+    by (rule quasinorm_mult_distrib);
   also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
   finally; show "norm ([-] x) = norm x"; by simp;
 qed;
 
 
-subsection {* norm *};
+
+subsection {* Norms *};
+
 
 constdefs
   is_norm :: "['a set, 'a => real] => bool"
@@ -66,13 +78,16 @@
       & (norm x = 0r) = (x = <0>)";
 
 lemma is_normI [intro]: 
-  "ALL x: V.  is_quasinorm V norm  & (norm x = 0r) = (x = <0>) ==> is_norm V norm";
+  "ALL x: V.  is_quasinorm V norm  & (norm x = 0r) = (x = <0>) 
+  ==> is_norm V norm";
   by (unfold is_norm_def, force);
 
-lemma norm_is_quasinorm [intro!!]: "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
+lemma norm_is_quasinorm [intro!!]: 
+  "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
   by (unfold is_norm_def, force);
 
-lemma norm_zero_iff: "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
+lemma norm_zero_iff: 
+  "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
   by (unfold is_norm_def, force);
 
 lemma norm_ge_zero [intro!!]:
@@ -80,7 +95,8 @@
   by (unfold is_norm_def is_quasinorm_def, force);
 
 
-subsection {* normed vector space *};
+subsection {* Normed vector spaces *};
+
 
 constdefs
   is_normed_vectorspace :: "['a set, 'a => real] => bool"
@@ -89,16 +105,20 @@
       is_norm V norm";
 
 lemma normed_vsI [intro]: 
-  "[| is_vectorspace V; is_norm V norm |] ==> is_normed_vectorspace V norm";
+  "[| is_vectorspace V; is_norm V norm |] 
+  ==> is_normed_vectorspace V norm";
   by (unfold is_normed_vectorspace_def) blast; 
 
-lemma normed_vs_vs [intro!!]: "is_normed_vectorspace V norm ==> is_vectorspace V";
+lemma normed_vs_vs [intro!!]: 
+  "is_normed_vectorspace V norm ==> is_vectorspace V";
   by (unfold is_normed_vectorspace_def) force;
 
-lemma normed_vs_norm [intro!!]: "is_normed_vectorspace V norm ==> is_norm V norm";
+lemma normed_vs_norm [intro!!]: 
+  "is_normed_vectorspace V norm ==> is_norm V norm";
   by (unfold is_normed_vectorspace_def, elim conjE);
 
-lemma normed_vs_norm_ge_zero [intro!!]: "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
+lemma normed_vs_norm_ge_zero [intro!!]: 
+  "[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x";
   by (unfold is_normed_vectorspace_def, rule, elim conjE);
 
 lemma normed_vs_norm_gt_zero [intro!!]: 
@@ -117,18 +137,23 @@
 qed;
 
 lemma normed_vs_norm_mult_distrib [intro!!]: 
-  "[| is_normed_vectorspace V norm; x:V |] ==> norm (a [*] x) = (rabs a) * (norm x)";
-  by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, rule normed_vs_norm);
+  "[| is_normed_vectorspace V norm; x:V |] 
+  ==> norm (a [*] x) = (rabs a) * (norm x)";
+  by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, 
+      rule normed_vs_norm);
 
 lemma normed_vs_norm_triangle_ineq [intro!!]: 
-  "[| is_normed_vectorspace V norm; x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y";
-  by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, rule normed_vs_norm);
+  "[| is_normed_vectorspace V norm; x:V; y:V |] 
+  ==> norm (x [+] y) <= norm x + norm y";
+  by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, 
+     rule normed_vs_norm);
 
 lemma subspace_normed_vs [intro!!]: 
   "[| is_subspace F E; is_vectorspace E; is_normed_vectorspace E norm |] 
    ==> is_normed_vectorspace F norm";
 proof (rule normed_vsI);
-  assume "is_subspace F E" "is_vectorspace E" "is_normed_vectorspace E norm";
+  assume "is_subspace F E" "is_vectorspace E" 
+         "is_normed_vectorspace E norm";
   show "is_vectorspace F"; ..;
   show "is_norm F norm"; 
   proof (intro is_normI ballI conjI);
@@ -149,4 +174,4 @@
   qed;
 qed;
 
-end;
+end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/ROOT.ML
--- a/src/HOL/Real/HahnBanach/ROOT.ML	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML	Fri Oct 08 16:40:27 1999 +0200
@@ -5,4 +5,5 @@
 The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
 *)
 
+time_use_thy "Bounds";
 time_use_thy "HahnBanach";
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,10 +3,13 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+
+header {* Subspaces *};
+
 theory Subspace = LinearSpace:;
 
 
-section {* subspaces *};
+subsection {* Subspaces *};
 
 constdefs
   is_subspace ::  "['a set, 'a set] => bool"
@@ -15,8 +18,9 @@
                        & a [*] x : U)";                            
 
 lemma subspaceI [intro]: 
-  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |]
-  \ ==> is_subspace U V";
+  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); 
+  ALL x:U. ALL a. a [*] x : U |]
+  ==> is_subspace U V";
   by (unfold is_subspace_def) simp;
 
 lemma "is_subspace U V ==> U ~= {}";
@@ -28,23 +32,27 @@
 lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
   by (unfold is_subspace_def) simp;
 
-lemma subspace_subsetD [simp, intro!!]: "[| is_subspace U V; x:U |]==> x:V";
+lemma subspace_subsetD [simp, intro!!]: 
+  "[| is_subspace U V; x:U |]==> x:V";
   by (unfold is_subspace_def) force;
 
-lemma subspace_add_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
-  by (unfold is_subspace_def) simp;
-
-lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
+lemma subspace_add_closed [simp, intro!!]: 
+  "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
   by (unfold is_subspace_def) simp;
 
-lemma subspace_diff_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
+lemma subspace_mult_closed [simp, intro!!]: 
+  "[| is_subspace U V; x: U |] ==> a [*] x: U";
+  by (unfold is_subspace_def) simp;
+
+lemma subspace_diff_closed [simp, intro!!]: 
+  "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
   by (unfold diff_def negate_def) simp;
 
-lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U";
- by (unfold negate_def) simp;
+lemma subspace_neg_closed [simp, intro!!]: 
+  "[| is_subspace U V; x: U |] ==> [-] x: U";
+  by (unfold negate_def) simp;
 
-
-theorem subspace_vs [intro!!]:
+lemma subspace_vs [intro!!]:
   "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
 proof -;
   assume "is_subspace U V" "is_vectorspace V";
@@ -65,7 +73,8 @@
   show "ALL x:V. ALL a. a [*] x : V"; by (simp!);
 qed;
 
-lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
+lemma subspace_trans: 
+  "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
 proof; 
   assume "is_subspace U V" "is_subspace V W";
   show "<0> : U"; ..;
@@ -88,7 +97,9 @@
 qed;
 
 
-section {* linear closure *};
+
+subsection {* Linear closure *};
+
 
 constdefs
   lin :: "'a => 'a set"
@@ -106,7 +117,8 @@
   show "x = 1r [*] x"; by (simp!);
 qed;
 
-lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
+lemma lin_subspace [intro!!]: 
+  "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
 proof;
   assume "is_vectorspace V" "x:V";
   show "<0> : lin x"; 
@@ -126,7 +138,8 @@
     thus "x1 [+] x2 : lin x";
     proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
       fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
-      show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2);
+      show "x1 [+] x2 = (a1 + a2) [*] x"; 
+        by (simp! add: vs_add_mult_distrib2);
     qed;
   qed;
 
@@ -141,14 +154,17 @@
   qed; 
 qed;
 
-
-lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
+lemma lin_vs [intro!!]: 
+  "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
 proof (rule subspace_vs);
   assume "is_vectorspace V" "x:V";
   show "is_subspace (lin x) V"; ..;
 qed;
 
-section {* sum of two vectorspaces *};
+
+
+subsection {* Sum of two vectorspaces *};
+
 
 constdefs 
   vectorspace_sum :: "['a set, 'a set] => 'a set"
@@ -159,11 +175,14 @@
 
 lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
 
-lemma vs_sumI [intro!!]: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
+lemma vs_sumI [intro!!]: 
+  "[| x: U; y:V; (t::'a) = x [+] y |] 
+  ==> (t::'a) : vectorspace_sum U V";
   by (unfold vectorspace_sum_def, intro CollectI bexI); 
 
 lemma subspace_vs_sum1 [intro!!]: 
-  "[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)";
+  "[| is_vectorspace U; is_vectorspace V |] 
+  ==> is_subspace U (vectorspace_sum U V)";
 proof; 
   assume "is_vectorspace U" "is_vectorspace V";
   show "<0> : U"; ..;
@@ -188,7 +207,6 @@
   ==> is_subspace (vectorspace_sum U V) E";
 proof; 
   assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E";
-
   show "<0> : vectorspace_sum U V";
   proof (intro vs_sumI);
     show "<0> : U"; ..;
@@ -202,24 +220,28 @@
     show "x:E"; by (simp!);
   qed;
   
-  show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V";
+  show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. 
+        x [+] y : vectorspace_sum U V";
   proof (intro ballI);
     fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V";
     thus "x [+] y : vectorspace_sum U V";
     proof (elim vs_sumE bexE, intro vs_sumI);
       fix ux vx uy vy; 
-      assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
+      assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" 
+             "y = uy [+] vy";
       show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!);
     qed (simp!)+;
   qed;
 
-  show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V";
+  show "ALL x:vectorspace_sum U V. ALL a. 
+        a [*] x : vectorspace_sum U V";
   proof (intro ballI allI);
     fix x a; assume "x:vectorspace_sum U V";
     thus "a [*] x : vectorspace_sum U V";
     proof (elim vs_sumE bexE, intro vs_sumI);
       fix a x u v; assume "u : U" "v : V" "x = u [+] v";
-      show "a [*] x = (a [*] u) [+] (a [*] v)"; by (simp! add: vs_add_mult_distrib1);
+      show "a [*] x = (a [*] u) [+] (a [*] v)"; 
+        by (simp! add: vs_add_mult_distrib1);
     qed (simp!)+;
   qed;
 qed;
@@ -233,17 +255,25 @@
 qed;
 
 
-section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
+
+subsection {* A special case *}
+
 
-lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; U Int V = {<0>}; 
-  u1:U; u2:U; v1:V; v2:V; u1 [+] v1 = u2 [+] v2 |] 
+text {* direct sum of a vectorspace and a linear closure of a vector 
+*};
+
+lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
+  U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 [+] v1 = u2 [+] v2 |] 
   ==> u1 = u2 & v1 = v2"; 
 proof; 
-  assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  "U Int V = {<0>}" 
-         "u1:U" "u2:U" "v1:V" "v2:V" "u1 [+] v1 = u2 [+] v2"; 
+  assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  
+    "U Int V = {<0>}" "u1:U" "u2:U" "v1:V" "v2:V" 
+    "u1 [+] v1 = u2 [+] v2"; 
   have eq: "u1 [-] u2 = v2 [-] v1"; by (simp! add: vs_add_diff_swap);
-  have u: "u1 [-] u2 : U"; by (simp!); with eq; have v': "v2 [-] v1 : U"; by simp; 
-  have v: "v2 [-] v1 : V"; by (simp!); with eq; have u': "u1 [-] u2 : V"; by simp;
+  have u: "u1 [-] u2 : U"; by (simp!); 
+  with eq; have v': "v2 [-] v1 : U"; by simp; 
+  have v: "v2 [-] v1 : V"; by (simp!); 
+  with eq; have u': "u1 [-] u2 : V"; by simp;
   
   show "u1 = u2";
   proof (rule vs_add_minus_eq);
@@ -256,8 +286,8 @@
   qed (rule);
 qed;
 
-lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; 
-  x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
+lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
+  x0 ~: H; x0 :E; x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
   ==> y1 = y2 & a1 = a2";
 proof;
   assume "is_vectorspace E" and h: "is_subspace H E"
@@ -281,7 +311,8 @@
             assume "a = 0r"; show ?thesis; by (simp!);
           next;
             assume "a ~= 0r"; 
-            from h; have "(rinv a) [*] a [*] x0 : H"; by (rule subspace_mult_closed) (simp!);
+            from h; have "(rinv a) [*] a [*] x0 : H"; 
+              by (rule subspace_mult_closed) (simp!);
             also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
             finally; have "x0 : H"; .;
             thus ?thesis; by contradiction;
@@ -306,10 +337,11 @@
 qed;
 
 lemma decomp1: 
-  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] 
+  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |]
   ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
 proof (rule, unfold split_paired_all);
-  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>";
+  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" 
+    "x0 ~= <0>";
   have h: "is_vectorspace H"; ..;
   fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
   have "y = t & a = 0r"; 
@@ -320,17 +352,17 @@
 lemma decomp3:
   "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
                 in (h y) + a * xi);
-      x = y [+] a [*] x0; 
-      is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
+  x = y [+] a [*] x0; is_vectorspace E; is_subspace H E;    
+  y:H; x0 ~: H; x0:E; x0 ~= <0> |]
   ==> h0 x = h y + a * xi";
 proof -;  
   assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
                     in (h y) + a * xi)"
-         "x = y [+] a [*] x0"
-         "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
-
+         "x = y [+] a [*] x0" "is_vectorspace E" "is_subspace H E" 
+         "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
   have "x : vectorspace_sum H (lin x0)"; 
-    by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
+    by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) 
+       force+;
   have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
   proof%%;
     show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
@@ -343,15 +375,17 @@
     proof -;
       show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
         by (rule Pair_fst_snd_eq [RS iffD2]);
-      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by (force!);
-      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by (force!);
-      from x y; show "fst xa = fst ya & snd xa = snd ya"; by (elim conjE) (rule decomp4, (simp!)+);
+      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; 
+        by (force!);
+      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; 
+        by (force!);
+      from x y; show "fst xa = fst ya & snd xa = snd ya"; 
+        by (elim conjE) (rule decomp4, (simp!)+);
     qed;
   qed;
-  hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; by (rule select1_equality) (force!);
+  hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; 
+    by (rule select1_equality) (force!);
   thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
 qed;
 
-end;
-
-
+end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/Zorn_Lemma.thy
--- a/src/HOL/Real/HahnBanach/Zorn_Lemma.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Zorn_Lemma.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,10 +3,12 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+header {* Zorn's Lemma *};
+
 theory Zorn_Lemma = Aux + Zorn:;
 
-
-lemma Zorn's_Lemma: "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==>
+lemma Zorn's_Lemma: 
+ "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==>
  EX y: S. ALL z: S. y <= z --> y = z";
 proof (rule Zorn_Lemma2);
   assume aS: "a:S";
@@ -33,6 +35,4 @@
   qed;
 qed;
 
-
-
-end;
+end;
\ No newline at end of file
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/document/notation.tex
--- a/src/HOL/Real/HahnBanach/document/notation.tex	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex	Fri Oct 08 16:40:27 1999 +0200
@@ -0,0 +1,22 @@
+
+\renewcommand{\isamarkupheader}[1]{\section{#1}}
+\parindent 0pt \parskip 0.5ex
+
+\newcommand{\name}[1]{\textsf{#1}}
+
+\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
+\newcommand{\var}[1]{{?\!#1}}
+\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
+\newcommand{\dsh}{\dshsym}
+
+\newcommand{\To}{\to}
+\newcommand{\dt}{{\mathpunct.}}
+\newcommand{\ap}{\mathbin{\!}}
+\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
+\newcommand{\all}[1]{\forall #1\dt\;}
+\newcommand{\ex}[1]{\exists #1\dt\;}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: 
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/document/root.tex
--- a/src/HOL/Real/HahnBanach/document/root.tex	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex	Fri Oct 08 16:40:27 1999 +0200
@@ -2,12 +2,20 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,pdfsetup}
 
+\input{notation}
+
 \begin{document}
 
-\title{The Hahn-Banach theorem for real vectorspaces}
+\title{The Hahn-Banach Theorem for Real Vectorspaces}
 \author{Gertrud Bauer}
 \maketitle
 
+\begin{abstract}
+  FIXME
+\end{abstract}
+
+\tableofcontents
+
 \input{session}
 
 \end{document}