# HG changeset patch
# User wenzelm
# Date 976999311 -3600
# Node ID c186279eecea889c8c79855b7aaee303c50036c4
# Parent  60c795d6bd9e3828bd813a9045dbb127f59f5f9b
tuned HOL/Real/HahnBanach;

diff -r 60c795d6bd9e -r c186279eecea src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/IsaMakefile	Sat Dec 16 21:41:51 2000 +0100
@@ -152,10 +152,8 @@
   Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
   Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
   Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
-  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/notation.tex \
-  Real/HahnBanach/document/bbb.sty Real/HahnBanach/document/root.bib \
-  Real/HahnBanach/document/root.tex \
-  Real/HahnBanach/document/notation.tex
+  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
+  Real/HahnBanach/document/root.tex
 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
 
 
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -11,139 +11,141 @@
 or elimination rules, respectively. *}
 
 lemmas [intro?] = isLub_isUb
-lemmas [intro?] = chainD 
+lemmas [intro?] = chainD
 lemmas chainE2 = chainD2 [elim_format, standard]
 
-text_raw {* \medskip *}
-text{* Lemmas about sets. *}
 
-lemma Int_singletonD: "[| A \<inter> B = {v}; x \<in> A; x \<in> B |] ==> x = v"
+text {* \medskip Lemmas about sets. *}
+
+lemma Int_singletonD: "A \<inter> B = {v} \<Longrightarrow> x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x = v"
   by (fast elim: equalityE)
 
-lemma set_less_imp_diff_not_empty: "H < E ==> \<exists>x0 \<in> E. x0 \<notin> H"
-  by (force simp add: psubset_eq)
+lemma set_less_imp_diff_not_empty: "H < E \<Longrightarrow> \<exists>x0 \<in> E. x0 \<notin> H"
+  by (auto simp add: psubset_eq)
+
 
-text_raw {* \medskip *}
-text{* Some lemmas about orders. *}
+text{* \medskip Some lemmas about orders. *}
 
-lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \<noteq> y"
+lemma lt_imp_not_eq: "x < (y::'a::order) \<Longrightarrow> x \<noteq> y"
   by (simp add: order_less_le)
 
-lemma le_noteq_imp_less: 
-  "[| x <= (r::'a::order); x \<noteq> r |] ==> x < r"
+lemma le_noteq_imp_less:
+  "x \<le> (r::'a::order) \<Longrightarrow> x \<noteq> r \<Longrightarrow> x < r"
 proof -
-  assume "x <= r" and ne:"x \<noteq> r"
-  hence "x < r | x = r" by (simp add: order_le_less)
+  assume "x \<le> r" and ne:"x \<noteq> r"
+  hence "x < r \<or> x = r" by (simp add: order_le_less)
   with ne show ?thesis by simp
 qed
 
-text_raw {* \medskip *}
-text{* Some lemmas for the reals. *}
 
-lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y"
+text {* \medskip Some lemmas for the reals. *}
+
+lemma real_add_minus_eq: "x - y = (#0::real) \<Longrightarrow> x = y"
   by simp
 
-lemma abs_minus_one: "abs (- (#1::real)) = #1" 
+lemma abs_minus_one: "abs (- (#1::real)) = #1"
   by simp
 
-lemma real_mult_le_le_mono1a: 
-  "[| (#0::real) <= z; x <= y |] ==> z * x  <= z * y"
+lemma real_mult_le_le_mono1a:
+  "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x  \<le> z * y"
 proof -
-  assume z: "(#0::real) <= z" and "x <= y"
-  hence "x < y | x = y" by (force simp add: order_le_less)
+  assume z: "(#0::real) \<le> z" and "x \<le> y"
+  hence "x < y \<or> x = y" by (auto simp add: order_le_less)
   thus ?thesis
-  proof (elim disjE) 
+  proof
     assume "x < y" show ?thesis by  (rule real_mult_le_less_mono2) simp
-  next 
+  next
     assume "x = y" thus ?thesis by simp
   qed
 qed
 
-lemma real_mult_le_le_mono2: 
-  "[| (#0::real) <= z; x <= y |] ==> x * z <= y * z"
+lemma real_mult_le_le_mono2:
+  "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> x * z \<le> y * z"
 proof -
-  assume "(#0::real) <= z" "x <= y"
-  hence "x < y | x = y" by (force simp add: order_le_less)
+  assume "(#0::real) \<le> z"  "x \<le> y"
+  hence "x < y \<or> x = y" by (auto simp add: order_le_less)
   thus ?thesis
-  proof (elim disjE) 
-    assume "x < y" show ?thesis by (rule real_mult_le_less_mono1) simp
-  next 
-    assume "x = y" thus ?thesis by simp
+  proof
+    assume "x < y"
+    show ?thesis by (rule real_mult_le_less_mono1) (simp!)
+  next
+    assume "x = y"
+    thus ?thesis by simp
   qed
 qed
 
-lemma real_mult_less_le_anti: 
-  "[| z < (#0::real); x <= y |] ==> z * y <= z * x"
+lemma real_mult_less_le_anti:
+  "z < (#0::real) \<Longrightarrow> x \<le> y \<Longrightarrow> z * y \<le> z * x"
 proof -
-  assume "z < #0" "x <= y"
+  assume "z < #0"  "x \<le> y"
   hence "#0 < - z" by simp
-  hence "#0 <= - z" by (rule real_less_imp_le)
-  hence "x * (- z) <= y * (- z)" 
+  hence "#0 \<le> - z" by (rule real_less_imp_le)
+  hence "x * (- z) \<le> y * (- z)"
     by (rule real_mult_le_le_mono2)
-  hence  "- (x * z) <= - (y * z)" 
+  hence  "- (x * z) \<le> - (y * z)"
     by (simp only: real_minus_mult_eq2)
   thus ?thesis by (simp only: real_mult_commute)
 qed
 
-lemma real_mult_less_le_mono: 
-  "[| (#0::real) < z; x <= y |] ==> z * x <= z * y"
-proof - 
-  assume "#0 < z" "x <= y"
-  have "#0 <= z" by (rule real_less_imp_le)
-  hence "x * z <= y * z" 
+lemma real_mult_less_le_mono:
+  "(#0::real) < z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y"
+proof -
+  assume "#0 < z"  "x \<le> y"
+  have "#0 \<le> z" by (rule real_less_imp_le)
+  hence "x * z \<le> y * z"
     by (rule real_mult_le_le_mono2)
   thus ?thesis by (simp only: real_mult_commute)
 qed
 
-lemma real_inverse_gt_zero1: "#0 < (x::real) ==> #0 < inverse x"
-proof - 
+lemma real_inverse_gt_zero1: "#0 < (x::real) \<Longrightarrow> #0 < inverse x"
+proof -
   assume "#0 < x"
   have "0 < x" by simp
   hence "0 < inverse x" by (rule real_inverse_gt_zero)
   thus ?thesis by simp
 qed
 
-lemma real_mult_inv_right1: "(x::real) \<noteq> #0 ==> x * inverse x = #1"
+lemma real_mult_inv_right1: "(x::real) \<noteq> #0 \<Longrightarrow> x * inverse x = #1"
   by simp
 
-lemma real_mult_inv_left1: "(x::real) \<noteq> #0 ==> inverse x * x = #1"
+lemma real_mult_inv_left1: "(x::real) \<noteq> #0 \<Longrightarrow> inverse x * x = #1"
   by simp
 
-lemma real_le_mult_order1a: 
-  "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"
+lemma real_le_mult_order1a:
+  "(#0::real) \<le> x \<Longrightarrow> #0 \<le> y \<Longrightarrow> #0 \<le> x * y"
 proof -
-  assume "#0 <= x" "#0 <= y"
-  have "[|0 <= x; 0 <= y|] ==> 0 <= x * y"  
+  assume "#0 \<le> x"  "#0 \<le> y"
+  have "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x * y"
     by (rule real_le_mult_order)
   thus ?thesis by (simp!)
 qed
 
-lemma real_mult_diff_distrib: 
+lemma real_mult_diff_distrib:
   "a * (- x - (y::real)) = - a * x - a * y"
 proof -
   have "- x - y = - x + - y" by simp
-  also have "a * ... = a * - x + a * - y" 
+  also have "a * ... = a * - x + a * - y"
     by (simp only: real_add_mult_distrib2)
-  also have "... = - a * x - a * y" 
+  also have "... = - a * x - a * y"
     by simp
   finally show ?thesis .
 qed
 
 lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y"
-proof - 
+proof -
   have "x - y = x + - y" by simp
-  also have "a * ... = a * x + a * - y" 
+  also have "a * ... = a * x + a * - y"
     by (simp only: real_add_mult_distrib2)
-  also have "... = a * x - a * y"   
+  also have "... = a * x - a * y"
     by simp
   finally show ?thesis .
 qed
 
-lemma real_minus_le: "- (x::real) <= y ==> - y <= x"
+lemma real_minus_le: "- (x::real) \<le> y \<Longrightarrow> - y \<le> x"
   by simp
 
-lemma real_diff_ineq_swap: 
-    "(d::real) - b <= c + a ==> - a - b <= c - d"
+lemma real_diff_ineq_swap:
+    "(d::real) - b \<le> c + a \<Longrightarrow> - a - b \<le> c - d"
   by simp
 
-end
\ No newline at end of file
+end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -6,128 +6,48 @@
 header {* Bounds *}
 
 theory Bounds = Main + Real:
-(*<*)
-subsection {* The sets of lower and upper bounds *}
 
-constdefs
-  is_LowerBound :: "('a::order) set => 'a set => 'a => bool"
-  "is_LowerBound A B == \<lambda>x. x \<in> A \<and> (\<forall>y \<in> B. x <= y)"
+text {*
+  A supremum\footnote{The definition of the supremum is based on one
+  in \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}}
+  of an ordered set @{text B} w.~r.~t. @{text A} is defined as a least
+  upper bound of @{text B}, which lies in @{text A}.
+*}
    
-  LowerBounds :: "('a::order) set => 'a set => 'a set"
-  "LowerBounds A B == Collect (is_LowerBound A B)"
-
-  is_UpperBound :: "('a::order) set => 'a set => 'a => bool"
-  "is_UpperBound A B == \<lambda>x. x \<in> A \<and> (\<forall>y \<in> B. y <= x)"
- 
-  UpperBounds :: "('a::order) set => 'a set => 'a set"
-  "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)
-
-translations
-  "UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (\<lambda>x. P))"
-  "UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P"
-  "LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\<lambda>x. P))"
-  "LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P"
-
-
-subsection {* Least and greatest elements *}
+text {*
+  If a supremum exists, then @{text "Sup A B"} is equal to the
+  supremum. *}
 
 constdefs
-  is_Least :: "('a::order) set => 'a => bool"
-  "is_Least B == is_LowerBound B B"
-
-  Least :: "('a::order) set => 'a"
-  "Least B == Eps (is_Least B)"
-
-  is_Greatest :: "('a::order) set => 'a => bool"
-  "is_Greatest B == is_UpperBound B B"
-
-  Greatest :: "('a::order) set => 'a" 
-  "Greatest B == Eps (is_Greatest B)"
+  is_Sup :: "('a::order) set \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool"
+  "is_Sup A B x \<equiv> isLub A B x"
 
-syntax
-  "_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}"
-
-
-subsection {* Infimum and Supremum *}
-(*>*)
-text {*
- A supremum\footnote{The definition of the supremum is based on one in
- \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}}  of
- an ordered set $B$ w.~r.~t. $A$ is defined as a least upper bound of
- $B$, which lies in $A$.
-*}
-   
-text{* If a supremum exists, then $\idt{Sup}\ap A\ap B$
-is equal to the supremum. *}
+  Sup :: "('a::order) set \<Rightarrow> 'a set \<Rightarrow> 'a"
+  "Sup A B \<equiv> Eps (is_Sup A B)"
 
-constdefs
-  is_Sup :: "('a::order) set => 'a set => 'a => bool"
-  "is_Sup A B x == isLub A B x"
-
-  Sup :: "('a::order) set => 'a set => 'a"
-  "Sup A B == Eps (is_Sup A B)"
-(*<*)
-constdefs
-  is_Inf :: "('a::order) set => 'a set => 'a => bool"
-  "is_Inf A B x == x \<in> A \<and>  is_Greatest (LowerBounds A B) x"
-
-  Inf :: "('a::order) set => 'a set => 'a"
-  "Inf A B == Eps (is_Inf A B)"
+text {*
+  The supremum of @{text B} is less than any upper bound of
+  @{text 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)
-
-translations
-  "SUP x:A. P" == "Sup A (Collect (\<lambda>x. P))"
-  "SUP x. P" == "SUP x:UNIV. P"
-  "INF x:A. P" == "Inf A (Collect (\<lambda>x. P))"
-  "INF x. P" == "INF x:UNIV. P"
-(*>*)
-text{* The supremum of $B$ is less than any upper bound
-of $B$.*}
-
-lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y"
+lemma sup_le_ub: "isUb A B y \<Longrightarrow> is_Sup A B s \<Longrightarrow> s \<le> y"
   by (unfold is_Sup_def, rule isLub_le_isUb)
 
-text {* The supremum $B$ is an upper bound for $B$. *}
+text {* The supremum @{text B} is an upper bound for @{text B}. *}
 
-lemma sup_ub: "y \<in> B ==> is_Sup A B s ==> y <= s"
+lemma sup_ub: "y \<in> B \<Longrightarrow> is_Sup A B s \<Longrightarrow> y \<le> s"
   by (unfold is_Sup_def, rule isLubD2)
 
-text{* The supremum of a non-empty set $B$ is greater
-than a lower bound of $B$. *}
+text {*
+  The supremum of a non-empty set @{text B} is greater than a lower
+  bound of @{text B}. *}
 
 lemma sup_ub1: 
-  "[| \<forall>y \<in> B. a <= y; is_Sup A B s; x \<in> B |] ==> a <= s"
+  "\<forall>y \<in> B. a \<le> y \<Longrightarrow> is_Sup A B s \<Longrightarrow> x \<in> B \<Longrightarrow> a \<le> s"
 proof - 
-  assume "\<forall>y \<in> B. a <= y" "is_Sup A B s" "x \<in> B"
-  have "a <= x" by (rule bspec)
-  also have "x <= s" by (rule sup_ub)
-  finally show "a <= s" .
+  assume "\<forall>y \<in> B. a \<le> y"  "is_Sup A B s"  "x \<in> B"
+  have "a \<le> x" by (rule bspec)
+  also have "x \<le> s" by (rule sup_ub)
+  finally show "a \<le> s" .
 qed
   
-end
\ No newline at end of file
+end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -9,377 +9,374 @@
 
 subsection {* Continuous linear forms*}
 
-text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$
-is \emph{continuous}, iff it is bounded, i.~e.
-\[\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}\]
-In our application no other functions than linear forms are considered,
-so we can define continuous linear forms as bounded linear forms:
+text {*
+  A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
+  is \emph{continuous}, iff it is bounded, i.~e.
+  \begin{center}
+  @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+  \end{center}
+  In our application no other functions than linear forms are
+  considered, so we can define continuous linear forms as bounded
+  linear forms:
 *}
 
 constdefs
   is_continuous ::
-  "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool" 
-  "is_continuous V norm f == 
-    is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x)"
+  "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
+  "is_continuous V norm f \<equiv>
+    is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x)"
 
-lemma continuousI [intro]: 
-  "[| is_linearform V f; !! x. x \<in> V ==> |f x| <= c * norm x |] 
-  ==> is_continuous V norm f"
+lemma continuousI [intro]:
+  "is_linearform V f \<Longrightarrow> (\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x)
+  \<Longrightarrow> is_continuous V norm f"
 proof (unfold is_continuous_def, intro exI conjI ballI)
-  assume r: "!! x. x \<in> V ==> |f x| <= c * norm x" 
-  fix x assume "x \<in> V" show "|f x| <= c * norm x" by (rule r)
+  assume r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x"
+  fix x assume "x \<in> V" show "\<bar>f x\<bar> \<le> c * norm x" by (rule r)
 qed
-  
-lemma continuous_linearform [intro?]: 
-  "is_continuous V norm f ==> is_linearform V f"
-  by (unfold is_continuous_def) force
+
+lemma continuous_linearform [intro?]:
+  "is_continuous V norm f \<Longrightarrow> is_linearform V f"
+  by (unfold is_continuous_def) blast
 
 lemma continuous_bounded [intro?]:
-  "is_continuous V norm f 
-  ==> \<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
-  by (unfold is_continuous_def) force
+  "is_continuous V norm f
+  \<Longrightarrow> \<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
+  by (unfold is_continuous_def) blast
 
 subsection{* The norm of a linear form *}
 
 
-text{* The least real number $c$ for which holds
-\[\All {x\in V}{|f\ap x| \leq c \cdot \norm x}\]
-is called the \emph{norm} of $f$.
+text {*
+  The least real number @{text c} for which holds
+  \begin{center}
+  @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+  \end{center}
+  is called the \emph{norm} of @{text f}.
 
-For non-trivial vector spaces $V \neq \{\zero\}$ the norm can be defined as 
-\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x} \] 
+  For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
+  defined as
+  \begin{center}
+  @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
+  \end{center}
 
-For the case $V = \{\zero\}$ the supremum would be taken from an
-empty set. Since $\bbbR$ is unbounded, there would be no supremum.  To
-avoid this situation it must be guaranteed that there is an element in
-this set. This element must be ${} \ge 0$ so that
-$\idt{function{\dsh}norm}$ has the norm properties. Furthermore it
-does not have to change the norm in all other cases, so it must be
-$0$, as all other elements of are ${} \ge 0$.
+  For the case @{text "V = {0}"} the supremum would be taken from an
+  empty set. Since @{text \<real>} is unbounded, there would be no supremum.
+  To avoid this situation it must be guaranteed that there is an
+  element in this set. This element must be @{text "{} \<ge> 0"} so that
+  @{text function_norm} has the norm properties. Furthermore
+  it does not have to change the norm in all other cases, so it must
+  be @{text 0}, as all other elements of are @{text "{} \<ge> 0"}.
 
-Thus we define the set $B$ the supremum is taken from as
-\[
-\{ 0 \} \Union \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
- \]
+  Thus we define the set @{text B} the supremum is taken from as
+  \begin{center}
+  @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
+  \end{center}
+*}
+
+constdefs
+  B :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a::{plus, minus, zero} \<Rightarrow> real) \<Rightarrow> real set"
+  "B V norm f \<equiv>
+  {#0} \<union> {\<bar>f x\<bar> * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
+
+text {*
+  @{text n} is the function norm of @{text f}, iff @{text n} is the
+  supremum of @{text B}.
 *}
 
 constdefs
-  B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"
-  "B V norm f == 
-  {#0} \<union> {|f x| * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
+  is_function_norm ::
+  "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"
+  "is_function_norm f V norm fn \<equiv> is_Sup UNIV (B V norm f) fn"
 
-text{* $n$ is the function norm of $f$, iff 
-$n$ is the supremum of $B$. 
+text {*
+  @{text function_norm} is equal to the supremum of @{text B}, if the
+  supremum exists. Otherwise it is undefined.
 *}
 
-constdefs 
-  is_function_norm :: 
-  " ['a::{minus,plus,zero}  => real, 'a set, 'a => real] => real => bool"
-  "is_function_norm f V norm fn == is_Sup UNIV (B V norm f) fn"
+constdefs
+  function_norm :: "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"
+  "function_norm f V norm \<equiv> Sup UNIV (B V norm f)"
 
-text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
-if the supremum exists. Otherwise it is undefined. *}
-
-constdefs 
-  function_norm :: " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real"
-  "function_norm f V norm == Sup UNIV (B V norm f)"
-
-syntax   
-  function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\<parallel>_\<parallel>_,_")
+syntax
+  function_norm :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"  ("\<parallel>_\<parallel>_,_")
 
 lemma B_not_empty: "#0 \<in> B V norm f"
-  by (unfold B_def, force)
-
-text {* The following lemma states that every continuous linear form
-on a normed space $(V, \norm{\cdot})$ has a function norm. *}
+  by (unfold B_def) blast
 
-lemma ex_fnorm [intro?]: 
-  "[| is_normed_vectorspace V norm; is_continuous V norm f|]
-     ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm" 
-proof (unfold function_norm_def is_function_norm_def 
+text {*
+  The following lemma states that every continuous linear form on a
+  normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
+*}
+
+lemma ex_fnorm [intro?]:
+  "is_normed_vectorspace V norm \<Longrightarrow> is_continuous V norm f
+     \<Longrightarrow> is_function_norm f V norm \<parallel>f\<parallel>V,norm"
+proof (unfold function_norm_def is_function_norm_def
   is_continuous_def Sup_def, elim conjE, rule someI2_ex)
   assume "is_normed_vectorspace V norm"
-  assume "is_linearform V f" 
-  and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
+  assume "is_linearform V f"
+  and e: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
 
-  txt {* The existence of the supremum is shown using the 
+  txt {* The existence of the supremum is shown using the
   completeness of the reals. Completeness means, that
-  every non-empty bounded set of reals has a 
+  every non-empty bounded set of reals has a
   supremum. *}
-  show  "\<exists>a. is_Sup UNIV (B V norm f) a" 
+  show  "\<exists>a. is_Sup UNIV (B V norm f) a"
   proof (unfold is_Sup_def, rule reals_complete)
 
-    txt {* First we have to show that $B$ is non-empty: *} 
+    txt {* First we have to show that @{text B} is non-empty: *}
 
-    show "\<exists>X. X \<in> B V norm f" 
-    proof (intro exI)
-      show "#0 \<in> (B V norm f)" by (unfold B_def, force)
+    show "\<exists>X. X \<in> B V norm f"
+    proof
+      show "#0 \<in> (B V norm f)" by (unfold B_def) blast
     qed
 
-    txt {* Then we have to show that $B$ is bounded: *}
+    txt {* Then we have to show that @{text B} is bounded: *}
 
     from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
     proof
 
-      txt {* We know that $f$ is bounded by some value $c$. *}  
-  
-      fix c assume a: "\<forall>x \<in> V. |f x| <= c * norm x"
-      def b == "max c #0"
+      txt {* We know that @{text f} is bounded by some value @{text c}. *}
+
+      fix c assume a: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
+      def b \<equiv> "max c #0"
 
       show "?thesis"
-      proof (intro exI isUbI setleI ballI, unfold B_def, 
-	elim UnE CollectE exE conjE singletonE)
+      proof (intro exI isUbI setleI ballI, unfold B_def,
+        elim UnE CollectE exE conjE singletonE)
 
-        txt{* To proof the thesis, we have to show that there is 
-        some constant $b$, such that $y \leq b$ for all $y\in B$. 
-        Due to the definition of $B$ there are two cases for
-        $y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}
+        txt {* To proof the thesis, we have to show that there is some
+        constant @{text b}, such that @{text "y \<le> b"} for all
+        @{text "y \<in> B"}. Due to the definition of @{text B} there are
+        two cases for @{text "y \<in> B"}.  If @{text "y = 0"} then
+        @{text "y \<le> max c 0"}: *}
 
-	fix y assume "y = (#0::real)"
-        show "y <= b" by (simp! add: le_maxI2)
+        fix y assume "y = (#0::real)"
+        show "y \<le> b" by (simp! add: le_maxI2)
 
-        txt{* The second case is 
-        $y = {|f\ap x|}/{\norm x}$ for some 
-        $x\in V$ with $x \neq \zero$. *}
+        txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
+        @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
 
       next
-	fix x y
-        assume "x \<in> V" "x \<noteq> 0" (***
+        fix x y
+        assume "x \<in> V"  "x \<noteq> 0"
+
+        txt {* The thesis follows by a short calculation using the
+        fact that @{text f} is bounded. *}
 
-         have ge: "#0 <= inverse (norm x)";
-          by (rule real_less_imp_le, rule real_inverse_gt_zero, 
-                rule normed_vs_norm_gt_zero); ( ***
-          proof (rule real_less_imp_le);
-            show "#0 < inverse (norm x)";
-            proof (rule real_inverse_gt_zero);
-              show "#0 < norm x"; ..;
-            qed;
-          qed; *** )
-        have nz: "norm x \<noteq> #0" 
-          by (rule not_sym, rule lt_imp_not_eq, 
-              rule normed_vs_norm_gt_zero) (***
-          proof (rule not_sym);
-            show "#0 \<noteq> norm x"; 
-            proof (rule lt_imp_not_eq);
-              show "#0 < norm x"; ..;
-            qed;
-          qed; ***)***)
-
-        txt {* The thesis follows by a short calculation using the 
-        fact that $f$ is bounded. *}
-    
-        assume "y = |f x| * inverse (norm x)"
-        also have "... <= c * norm x * inverse (norm x)"
+        assume "y = \<bar>f x\<bar> * inverse (norm x)"
+        also have "... \<le> c * norm x * inverse (norm x)"
         proof (rule real_mult_le_le_mono2)
-          show "#0 <= inverse (norm x)"
-            by (rule real_less_imp_le, rule real_inverse_gt_zero1, 
+          show "#0 \<le> inverse (norm x)"
+            by (rule real_less_imp_le, rule real_inverse_gt_zero1,
                 rule normed_vs_norm_gt_zero)
-          from a show "|f x| <= c * norm x" ..
+          from a show "\<bar>f x\<bar> \<le> c * norm x" ..
         qed
-        also have "... = c * (norm x * inverse (norm x))" 
+        also have "... = c * (norm x * inverse (norm x))"
           by (rule real_mult_assoc)
-        also have "(norm x * inverse (norm x)) = (#1::real)" 
+        also have "(norm x * inverse (norm x)) = (#1::real)"
         proof (rule real_mult_inv_right1)
-          show nz: "norm x \<noteq> #0" 
-            by (rule not_sym, rule lt_imp_not_eq, 
+          show nz: "norm x \<noteq> #0"
+            by (rule not_sym, rule lt_imp_not_eq,
               rule normed_vs_norm_gt_zero)
         qed
-        also have "c * ... <= b " by (simp! add: le_maxI1)
-	finally show "y <= b" .
+        also have "c * ... \<le> b " by (simp! add: le_maxI1)
+        finally show "y \<le> b" .
       qed simp
     qed
   qed
 qed
 
-text {* The norm of a continuous function is always $\geq 0$. *}
+text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
 
-lemma fnorm_ge_zero [intro?]: 
-  "[| is_continuous V norm f; is_normed_vectorspace V norm |]
-   ==> #0 <= \<parallel>f\<parallel>V,norm"
+lemma fnorm_ge_zero [intro?]:
+  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm
+   \<Longrightarrow> #0 \<le> \<parallel>f\<parallel>V,norm"
 proof -
-  assume c: "is_continuous V norm f" 
+  assume c: "is_continuous V norm f"
      and n: "is_normed_vectorspace V norm"
 
-  txt {* The function norm is defined as the supremum of $B$. 
-  So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided
-  the supremum exists and $B$ is not empty. *}
+  txt {* The function norm is defined as the supremum of @{text B}.
+  So it is @{text "\<ge> 0"} if all elements in @{text B} are
+  @{text "\<ge> 0"}, provided the supremum exists and @{text B} is not
+  empty. *}
 
-  show ?thesis 
+  show ?thesis
   proof (unfold function_norm_def, rule sup_ub1)
-    show "\<forall>x \<in> (B V norm f). #0 <= x" 
+    show "\<forall>x \<in> (B V norm f). #0 \<le> x"
     proof (intro ballI, unfold B_def,
-           elim UnE singletonE CollectE exE conjE) 
+           elim UnE singletonE CollectE exE conjE)
       fix x r
-      assume "x \<in> V" "x \<noteq> 0" 
-        and r: "r = |f x| * inverse (norm x)"
+      assume "x \<in> V"  "x \<noteq> 0"
+        and r: "r = \<bar>f x\<bar> * inverse (norm x)"
 
-      have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)
-      have "#0 <= inverse (norm x)" 
+      have ge: "#0 \<le> \<bar>f x\<bar>" by (simp! only: abs_ge_zero)
+      have "#0 \<le> inverse (norm x)"
         by (rule real_less_imp_le, rule real_inverse_gt_zero1, rule)(***
         proof (rule real_less_imp_le);
-          show "#0 < inverse (norm x)"; 
+          show "#0 < inverse (norm x)";
           proof (rule real_inverse_gt_zero);
             show "#0 < norm x"; ..;
           qed;
         qed; ***)
-      with ge show "#0 <= r"
+      with ge show "#0 \<le> r"
        by (simp only: r, rule real_le_mult_order1a)
     qed (simp!)
 
-    txt {* Since $f$ is continuous the function norm exists: *}
+    txt {* Since @{text f} is continuous the function norm exists: *}
 
     have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" ..
-    thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" 
+    thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
       by (unfold is_function_norm_def function_norm_def)
 
-    txt {* $B$ is non-empty by construction: *}
+    txt {* @{text B} is non-empty by construction: *}
 
     show "#0 \<in> B V norm f" by (rule B_not_empty)
   qed
 qed
-  
-text{* \medskip The fundamental property of function norms is: 
-\begin{matharray}{l}
-| f\ap x | \leq {\fnorm {f}} \cdot {\norm x}  
-\end{matharray}
+
+text {*
+  \medskip The fundamental property of function norms is:
+  \begin{center}
+  @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+  \end{center}
 *}
 
-lemma norm_fx_le_norm_f_norm_x: 
-  "[| is_continuous V norm f; is_normed_vectorspace V norm; x \<in> V |] 
-    ==> |f x| <= \<parallel>f\<parallel>V,norm * norm x"
-proof - 
-  assume "is_normed_vectorspace V norm" "x \<in> V" 
+lemma norm_fx_le_norm_f_norm_x:
+  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow> x \<in> V
+    \<Longrightarrow> \<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x"
+proof -
+  assume "is_normed_vectorspace V norm"  "x \<in> V"
   and c: "is_continuous V norm f"
   have v: "is_vectorspace V" ..
 
- txt{* The proof is by case analysis on $x$. *}
- 
+ txt{* The proof is by case analysis on @{text x}. *}
+
   show ?thesis
   proof cases
 
-    txt {* For the case $x = \zero$ the thesis follows
-    from the linearity of $f$: for every linear function
-    holds $f\ap \zero = 0$. *}
+    txt {* For the case @{text "x = 0"} the thesis follows from the
+    linearity of @{text f}: for every linear function holds
+    @{text "f 0 = 0"}. *}
 
     assume "x = 0"
-    have "|f x| = |f 0|" by (simp!)
+    have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by (simp!)
     also from v continuous_linearform have "f 0 = #0" ..
     also note abs_zero
-    also have "#0 <= \<parallel>f\<parallel>V,norm * norm x"
+    also have "#0 \<le> \<parallel>f\<parallel>V,norm * norm x"
     proof (rule real_le_mult_order1a)
-      show "#0 <= \<parallel>f\<parallel>V,norm" ..
-      show "#0 <= norm x" ..
+      show "#0 \<le> \<parallel>f\<parallel>V,norm" ..
+      show "#0 \<le> norm x" ..
     qed
-    finally 
-    show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
+    finally
+    show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
 
   next
     assume "x \<noteq> 0"
     have n: "#0 < norm x" ..
-    hence nz: "norm x \<noteq> #0" 
+    hence nz: "norm x \<noteq> #0"
       by (simp only: lt_imp_not_eq)
 
-    txt {* For the case $x\neq \zero$ we derive the following
-    fact from the definition of the function norm:*}
+    txt {* For the case @{text "x \<noteq> 0"} we derive the following fact
+    from the definition of the function norm:*}
 
-    have l: "|f x| * inverse (norm x) <= \<parallel>f\<parallel>V,norm"
+    have l: "\<bar>f x\<bar> * inverse (norm x) \<le> \<parallel>f\<parallel>V,norm"
     proof (unfold function_norm_def, rule sup_ub)
       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 "|f x| * inverse (norm x) \<in> B V norm f" 
+      show "\<bar>f x\<bar> * inverse (norm x) \<in> B V norm f"
         by (unfold B_def, intro UnI2 CollectI exI [of _ x]
             conjI, simp)
     qed
 
     txt {* The thesis now follows by a short calculation: *}
 
-    have "|f x| = |f x| * #1" by (simp!)
-    also from nz have "#1 = inverse (norm x) * norm x" 
+    have "\<bar>f x\<bar> = \<bar>f x\<bar> * #1" by (simp!)
+    also from nz have "#1 = inverse (norm x) * norm x"
       by (simp add: real_mult_inv_left1)
-    also have "|f x| * ... = |f x| * inverse (norm x) * norm x"
+    also have "\<bar>f x\<bar> * ... = \<bar>f x\<bar> * inverse (norm x) * norm x"
       by (simp! add: real_mult_assoc)
-    also from n l have "... <= \<parallel>f\<parallel>V,norm * norm x"
+    also from n l have "... \<le> \<parallel>f\<parallel>V,norm * norm x"
       by (simp add: real_mult_le_le_mono2)
-    finally show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
+    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
   qed
 qed
 
-text{* \medskip The function norm is the least positive real number for 
-which the following inequation holds:
-\begin{matharray}{l}
-| f\ap x | \leq c \cdot {\norm x}  
-\end{matharray} 
+text {*
+  \medskip The function norm is the least positive real number for
+  which the following inequation holds:
+  \begin{center}
+  @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+  \end{center}
 *}
 
-lemma fnorm_le_ub: 
-  "[| is_continuous V norm f; is_normed_vectorspace V norm; 
-     \<forall>x \<in> V. |f x| <= c * norm x; #0 <= c |]
-  ==> \<parallel>f\<parallel>V,norm <= c"
+lemma fnorm_le_ub:
+  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow>
+     \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x \<Longrightarrow> #0 \<le> c
+  \<Longrightarrow> \<parallel>f\<parallel>V,norm \<le> c"
 proof (unfold function_norm_def)
-  assume "is_normed_vectorspace V norm" 
+  assume "is_normed_vectorspace V norm"
   assume c: "is_continuous V norm f"
-  assume fb: "\<forall>x \<in> V. |f x| <= c * norm x"
-    and "#0 <= c"
+  assume fb: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
+    and "#0 \<le> c"
 
-  txt {* Suppose the inequation holds for some $c\geq 0$.
-  If $c$ is an upper bound of $B$, then $c$ is greater 
-  than the function norm since the function norm is the
-  least upper bound.
-  *}
+  txt {* Suppose the inequation holds for some @{text "c \<ge> 0"}.  If
+  @{text c} is an upper bound of @{text B}, then @{text c} is greater
+  than the function norm since the function norm is the least upper
+  bound.  *}
 
-  show "Sup UNIV (B V norm f) <= c" 
+  show "Sup UNIV (B V norm f) \<le> 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))" 
-      by (simp! add: is_function_norm_def function_norm_def) 
-  
-    txt {* $c$ is an upper bound of $B$, i.e. every
-    $y\in B$ is less than $c$. *}
+    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"  
+    txt {* @{text c} is an upper bound of @{text B}, i.e. every
+    @{text "y \<in> B"} is less than @{text c}. *}
+
+    show "isUb UNIV (B V norm f) c"
     proof (intro isUbI setleI ballI)
       fix y assume "y \<in> B V norm f"
-      thus le: "y <= c"
+      thus le: "y \<le> c"
       proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
 
-       txt {* The first case for $y\in B$ is $y=0$. *}
+       txt {* The first case for @{text "y \<in> B"} is @{text "y = 0"}. *}
 
         assume "y = #0"
-        show "y <= c" by (force!)
+        show "y \<le> c" by (blast!)
 
-        txt{* The second case is 
-        $y = {|f\ap x|}/{\norm x}$ for some 
-        $x\in V$ with $x \neq \zero$. *}  
+        txt{* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
+        @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
 
       next
-	fix x 
-        assume "x \<in> V" "x \<noteq> 0" 
+        fix x
+        assume "x \<in> V"  "x \<noteq> 0"
 
-        have lz: "#0 < norm x" 
+        have lz: "#0 < norm x"
           by (simp! add: normed_vs_norm_gt_zero)
-          
-        have nz: "norm x \<noteq> #0" 
+
+        have nz: "norm x \<noteq> #0"
         proof (rule not_sym)
           from lz show "#0 \<noteq> norm x"
             by (simp! add: order_less_imp_not_eq)
         qed
-            
-	from lz have "#0 < inverse (norm x)"
-	  by (simp! add: real_inverse_gt_zero1)
-	hence inverse_gez: "#0 <= inverse (norm x)"
+
+        from lz have "#0 < inverse (norm x)"
+          by (simp! add: real_inverse_gt_zero1)
+        hence inverse_gez: "#0 \<le> inverse (norm x)"
           by (rule real_less_imp_le)
 
-	assume "y = |f x| * inverse (norm x)" 
-	also from inverse_gez have "... <= c * norm x * inverse (norm x)"
-	  proof (rule real_mult_le_le_mono2)
-	    show "|f x| <= c * norm x" by (rule bspec)
-	  qed
-	also have "... <= c" by (simp add: nz real_mult_assoc)
-	finally show ?thesis .
+        assume "y = \<bar>f x\<bar> * inverse (norm x)"
+        also from inverse_gez have "... \<le> c * norm x * inverse (norm x)"
+          proof (rule real_mult_le_le_mono2)
+            show "\<bar>f x\<bar> \<le> c * norm x" by (rule bspec)
+          qed
+        also have "... \<le> c" by (simp add: nz real_mult_assoc)
+        finally show ?thesis .
       qed
-    qed force
+    qed blast
   qed
 qed
 
-end
\ No newline at end of file
+end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -9,75 +9,82 @@
 
 subsection {* The graph of a function *}
 
-text{* We define the \emph{graph} of a (real) function $f$ with
-domain $F$ as the set 
-\[
-\{(x, f\ap x). \ap x \in F\}
-\]
-So we are modeling partial functions by specifying the domain and 
-the mapping function. We use the term ``function'' also for its graph.
+text {*
+  We define the \emph{graph} of a (real) function @{text f} with
+  domain @{text F} as the set
+  \begin{center}
+  @{text "{(x, f x). x \<in> F}"}
+  \end{center}
+  So we are modeling partial functions by specifying the domain and
+  the mapping function. We use the term ``function'' also for its
+  graph.
 *}
 
 types 'a graph = "('a * real) set"
 
 constdefs
-  graph :: "['a set, 'a => real] => 'a graph "
-  "graph F f == {(x, f x) | x. x \<in> F}" 
+  graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph "
+  "graph F f \<equiv> {(x, f x) | x. x \<in> F}"
 
-lemma graphI [intro?]: "x \<in> F ==> (x, f x) \<in> graph F f"
-  by (unfold graph_def, intro CollectI exI) force
+lemma graphI [intro?]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
+  by (unfold graph_def, intro CollectI exI) blast
 
-lemma graphI2 [intro?]: "x \<in> F ==> \<exists>t\<in> (graph F f). t = (x, f x)"
-  by (unfold graph_def, force)
+lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t\<in> (graph F f). t = (x, f x)"
+  by (unfold graph_def) blast
 
-lemma graphD1 [intro?]: "(x, y) \<in> graph F f ==> x \<in> F"
-  by (unfold graph_def, elim CollectE exE) force
+lemma graphD1 [intro?]: "(x, y) \<in> graph F f \<Longrightarrow> x \<in> F"
+  by (unfold graph_def) blast
 
-lemma graphD2 [intro?]: "(x, y) \<in> graph H h ==> y = h x"
-  by (unfold graph_def, elim CollectE exE) force 
+lemma graphD2 [intro?]: "(x, y) \<in> graph H h \<Longrightarrow> y = h x"
+  by (unfold graph_def) blast
+
 
 subsection {* Functions ordered by domain extension *}
 
-text{* A function $h'$ is an extension of $h$, iff the graph of 
-$h$ is a subset of the graph of $h'$.*}
+text {* A function @{text h'} is an extension of @{text h}, iff the
+  graph of @{text h} is a subset of the graph of @{text h'}. *}
 
-lemma graph_extI: 
-  "[| !! x. x \<in> H ==> h x = h' x; H <= H'|]
-  ==> graph H h <= graph H' h'"
-  by (unfold graph_def, force)
+lemma graph_extI:
+  "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'
+  \<Longrightarrow> graph H h \<subseteq> graph H' h'"
+  by (unfold graph_def) blast
 
-lemma graph_extD1 [intro?]: 
-  "[| graph H h <= graph H' h'; x \<in> H |] ==> h x = h' x"
-  by (unfold graph_def, force)
+lemma graph_extD1 [intro?]:
+  "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
+  by (unfold graph_def) blast
 
-lemma graph_extD2 [intro?]: 
-  "[| graph H h <= graph H' h' |] ==> H <= H'"
-  by (unfold graph_def, force)
+lemma graph_extD2 [intro?]:
+  "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
+  by (unfold graph_def) blast
 
 subsection {* Domain and function of a graph *}
 
-text{* The inverse functions to $\idt{graph}$ are $\idt{domain}$ and 
-$\idt{funct}$.*}
+text {*
+  The inverse functions to @{text graph} are @{text domain} and
+  @{text funct}.
+*}
 
 constdefs
-  domain :: "'a graph => 'a set" 
-  "domain g == {x. \<exists>y. (x, y) \<in> g}"
+  domain :: "'a graph \<Rightarrow> 'a set"
+  "domain g \<equiv> {x. \<exists>y. (x, y) \<in> g}"
 
-  funct :: "'a graph => ('a => real)"
-  "funct g == \<lambda>x. (SOME y. (x, y) \<in> g)"
+  funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
+  "funct g \<equiv> \<lambda>x. (SOME y. (x, y) \<in> g)"
 
 
-text {* The following lemma states that $g$ is the graph of a function
-if the relation induced by $g$ is unique. *}
+text {*
+  The following lemma states that @{text g} is the graph of a function
+  if the relation induced by @{text g} is unique.
+*}
 
-lemma graph_domain_funct: 
-  "(!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y) 
-  ==> graph (domain g) (funct g) = g"
+lemma graph_domain_funct:
+  "(\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y)
+  \<Longrightarrow> graph (domain g) (funct g) = g"
 proof (unfold domain_def funct_def graph_def, auto)
   fix a b assume "(a, b) \<in> g"
   show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
   show "\<exists>y. (a, y) \<in> g" ..
-  assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y"
+  assume uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
   show "b = (SOME y. (a, y) \<in> g)"
   proof (rule some_equality [symmetric])
     fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
@@ -88,47 +95,49 @@
 
 subsection {* Norm-preserving extensions of a function *}
 
-text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on 
-$E$. The set of all linear extensions of $f$, to superspaces $H$ of 
-$F$, which are bounded by $p$, is defined as follows. *}
-
+text {*
+  Given a linear form @{text f} on the space @{text F} and a seminorm
+  @{text p} on @{text E}. The set of all linear extensions of @{text
+  f}, to superspaces @{text H} of @{text F}, which are bounded by
+  @{text p}, is defined as follows.
+*}
 
 constdefs
-  norm_pres_extensions :: 
-    "['a::{plus, minus, zero} set, 'a  => real, 'a set, 'a => real] 
-    => 'a graph set"
-    "norm_pres_extensions E p F f 
-    == {g. \<exists>H h. graph H h = g 
-                \<and> is_linearform H h 
+  norm_pres_extensions ::
+    "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
+    \<Rightarrow> 'a graph set"
+    "norm_pres_extensions E p F f
+    \<equiv> {g. \<exists>H h. graph H h = g
+                \<and> is_linearform H h
                 \<and> is_subspace H E
                 \<and> is_subspace F H
-                \<and> graph F f <= graph H h
-                \<and> (\<forall>x \<in> H. h x <= p x)}"
-                       
-lemma norm_pres_extension_D:  
+                \<and> graph F f \<subseteq> graph H h
+                \<and> (\<forall>x \<in> H. h x \<le> p x)}"
+
+lemma norm_pres_extension_D:
   "g \<in> norm_pres_extensions E p F f
-  ==> \<exists>H h. graph H h = g 
-            \<and> is_linearform H h 
+  \<Longrightarrow> \<exists>H h. graph H h = g
+            \<and> is_linearform H h
             \<and> is_subspace H E
             \<and> is_subspace F H
-            \<and> graph F f <= graph H h
-            \<and> (\<forall>x \<in> H. h x <= p x)"
-  by (unfold norm_pres_extensions_def) force
+            \<and> graph F f \<subseteq> graph H h
+            \<and> (\<forall>x \<in> H. h x \<le> p x)"
+  by (unfold norm_pres_extensions_def) blast
 
-lemma norm_pres_extensionI2 [intro]:  
-  "[| is_linearform H h; is_subspace H E; is_subspace F H;
-  graph F f <= graph H h; \<forall>x \<in> H. h x <= p x |]
-  ==> (graph H h \<in> norm_pres_extensions E p F f)"
- by (unfold norm_pres_extensions_def) force
+lemma norm_pres_extensionI2 [intro]:
+  "is_linearform H h \<Longrightarrow> is_subspace H E \<Longrightarrow> is_subspace F H \<Longrightarrow>
+  graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x
+  \<Longrightarrow> (graph H h \<in> norm_pres_extensions E p F f)"
+ by (unfold norm_pres_extensions_def) blast
 
-lemma norm_pres_extensionI [intro]:  
-  "\<exists>H h. graph H h = g 
-         \<and> is_linearform H h    
+lemma norm_pres_extensionI [intro]:
+  "\<exists>H h. graph H h = g
+         \<and> is_linearform H h
          \<and> is_subspace H E
          \<and> is_subspace F H
-         \<and> graph F f <= graph H h
-         \<and> (\<forall>x \<in> H. h x <= p x)
-  ==> g \<in> norm_pres_extensions E p F f"
-  by (unfold norm_pres_extensions_def) force
+         \<and> graph F f \<subseteq> graph H h
+         \<and> (\<forall>x \<in> H. h x \<le> p x)
+  \<Longrightarrow> g \<in> norm_pres_extensions E p F f"
+  by (unfold norm_pres_extensions_def) blast
 
-end
\ No newline at end of file
+end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -5,152 +5,142 @@
 
 header {* The Hahn-Banach Theorem *}
 
-theory HahnBanach = HahnBanachLemmas: 
+theory HahnBanach = HahnBanachLemmas:
 
 text {*
-  We present the proof of two different versions of the Hahn-Banach 
+  We present the proof of two different versions of the Hahn-Banach
   Theorem, closely following \cite[\S36]{Heuser:1986}.
 *}
 
 subsection {* The Hahn-Banach Theorem for vector spaces *}
 
 text {*
-{\bf Hahn-Banach Theorem.}\quad
-  Let $F$ be a subspace of a real vector space $E$, let $p$ be a semi-norm on
-  $E$, and $f$ be a linear form defined on $F$ such that $f$ is bounded by
-  $p$, i.e. $\All {x\in F} f\ap x \leq p\ap x$.  Then $f$ can be extended to
-  a linear form $h$ on $E$ such that $h$ is norm-preserving, i.e. $h$ is also
-  bounded by $p$.
+  \textbf{Hahn-Banach Theorem.} Let @{text F} be a subspace of a real
+  vector space @{text E}, let @{text p} be a semi-norm on @{text E},
+  and @{text f} be a linear form defined on @{text F} such that @{text
+  f} is bounded by @{text p}, i.e.  @{text "\<forall>x \<in> F. f x \<le> p x"}.  Then
+  @{text f} can be extended to a linear form @{text h} on @{text E}
+  such that @{text h} is norm-preserving, i.e. @{text h} is also
+  bounded by @{text p}.
+
+  \bigskip
+  \textbf{Proof Sketch.}
+  \begin{enumerate}
+
+  \item Define @{text M} as the set of norm-preserving extensions of
+  @{text f} to subspaces of @{text E}. The linear forms in @{text M}
+  are ordered by domain extension.
 
-\bigskip
-{\bf Proof Sketch.}
-\begin{enumerate}
-\item Define $M$ as the set of norm-preserving extensions of $f$ to subspaces
-  of $E$. The linear forms in $M$ are ordered by domain extension.
-\item We show that every non-empty chain in $M$ has an upper bound in $M$.
-\item With Zorn's Lemma we conclude that there is a maximal function $g$ in
-  $M$.
-\item The domain $H$ of $g$ is the whole space $E$, as shown by classical
-  contradiction:
-\begin{itemize}
-\item Assuming $g$ is not defined on whole $E$, it can still be extended in a
-  norm-preserving way to a super-space $H'$ of $H$.
-\item Thus $g$ can not be maximal. Contradiction!
-\end{itemize}
-\end{enumerate}
-\bigskip
+  \item We show that every non-empty chain in @{text M} has an upper
+  bound in @{text M}.
+
+  \item With Zorn's Lemma we conclude that there is a maximal function
+  @{text g} in @{text M}.
+
+  \item The domain @{text H} of @{text g} is the whole space @{text
+  E}, as shown by classical contradiction:
+
+  \begin{itemize}
+
+  \item Assuming @{text g} is not defined on whole @{text E}, it can
+  still be extended in a norm-preserving way to a super-space @{text
+  H'} of @{text H}.
+
+  \item Thus @{text g} can not be maximal. Contradiction!
+
+  \end{itemize}
+
+  \end{enumerate}
 *}
 
-(*
-text {* {\bf Theorem.} Let $f$ be a linear form defined on a subspace 
- $F$ of a real vector space $E$, such that $f$ is bounded by a seminorm 
- $p$. 
-
- Then $f$ can be extended  to a linear form $h$  on $E$ that is again
- bounded by $p$.
-
- \bigskip{\bf Proof Outline.}
- First we define the set $M$ of all norm-preserving extensions of $f$.
- We show that every chain in $M$ has an upper bound in $M$.
- With Zorn's lemma we can conclude that $M$ has a maximal element $g$.
- We further show by contradiction that the domain $H$ of $g$ is the whole
- vector space $E$. 
- If $H \neq E$, then $g$ can be extended in 
- a norm-preserving way to a greater vector space $H_0$. 
- So $g$ cannot be maximal in $M$.
- \bigskip
-*}
-*)
-
 theorem HahnBanach:
-  "[| is_vectorspace E; is_subspace F E; is_seminorm E p;
-  is_linearform F f; \<forall>x \<in> F. f x <= p x |] 
-  ==> \<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x)
-        \<and> (\<forall>x \<in> E. h x <= p x)"   
-    -- {* Let $E$ be a vector space, $F$ a subspace of $E$, $p$ a seminorm on $E$, *}
-    -- {* and $f$ a linear form on $F$ such that $f$ is bounded by $p$, *}
-    -- {* then $f$ can be extended to a linear form $h$ on $E$ in a norm-preserving way. \skp *}
+  "is_vectorspace E \<Longrightarrow> is_subspace F E \<Longrightarrow> is_seminorm E p
+  \<Longrightarrow> is_linearform F f \<Longrightarrow> \<forall>x \<in> F. f x \<le> p x
+  \<Longrightarrow> \<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
+    -- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *}
+    -- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *}
+    -- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *}
 proof -
-  assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
-   and "is_linearform F f" "\<forall>x \<in> F. f x <= p x"
+  assume "is_vectorspace E"  "is_subspace F E"  "is_seminorm E p"
+   and "is_linearform F f"  "\<forall>x \<in> F. f x \<le> p x"
   -- {* Assume the context of the theorem. \skp *}
-  def M == "norm_pres_extensions E p F f"
-  -- {* Define $M$ as the set of all norm-preserving extensions of $F$. \skp *}
+  def M \<equiv> "norm_pres_extensions E p F f"
+  -- {* Define @{text M} as the set of all norm-preserving extensions of @{text F}. \skp *}
   {
-    fix c assume "c \<in> chain M" "\<exists>x. x \<in> c"
+    fix c assume "c \<in> chain M"  "\<exists>x. x \<in> c"
     have "\<Union>c \<in> M"
-    -- {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
-    -- {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}
+    -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *}
+    -- {* @{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}. *}
     proof (unfold M_def, rule norm_pres_extensionI)
       show "\<exists>H h. graph H h = \<Union>c
-              \<and> is_linearform H h 
-              \<and> is_subspace H E 
-              \<and> is_subspace F H 
+              \<and> is_linearform H h
+              \<and> is_subspace H E
+              \<and> is_subspace F H
               \<and> graph F f \<subseteq> graph H h
-              \<and> (\<forall>x \<in> H. h x <= p x)"
+              \<and> (\<forall>x \<in> H. h x \<le> p x)"
       proof (intro exI conjI)
         let ?H = "domain (\<Union>c)"
         let ?h = "funct (\<Union>c)"
 
-        show a: "graph ?H ?h = \<Union>c" 
+        show a: "graph ?H ?h = \<Union>c"
         proof (rule graph_domain_funct)
-          fix x y z assume "(x, y) \<in> \<Union>c" "(x, z) \<in> \<Union>c"
+          fix x y z assume "(x, y) \<in> \<Union>c"  "(x, z) \<in> \<Union>c"
           show "z = y" by (rule sup_definite)
         qed
-        show "is_linearform ?H ?h" 
+        show "is_linearform ?H ?h"
           by (simp! add: sup_lf a)
-        show "is_subspace ?H E" 
+        show "is_subspace ?H E"
           by (rule sup_subE, rule a) (simp!)+
-        show "is_subspace F ?H" 
+        show "is_subspace F ?H"
           by (rule sup_supF, rule a) (simp!)+
-        show "graph F f \<subseteq> graph ?H ?h" 
+        show "graph F f \<subseteq> graph ?H ?h"
           by (rule sup_ext, rule a) (simp!)+
-        show "\<forall>x \<in> ?H. ?h x <= p x" 
+        show "\<forall>x \<in> ?H. ?h x \<le> p x"
           by (rule sup_norm_pres, rule a) (simp!)+
       qed
     qed
 
   }
-  hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x --> g = x" 
-  -- {* With Zorn's Lemma we can conclude that there is a maximal element in $M$.\skp *}
+  hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
+  -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *}
   proof (rule Zorn's_Lemma)
-    -- {* We show that $M$ is non-empty: *}
+    -- {* We show that @{text M} is non-empty: *}
     have "graph F f \<in> norm_pres_extensions E p F f"
     proof (rule norm_pres_extensionI2)
       have "is_vectorspace F" ..
       thus "is_subspace F F" ..
-    qed (blast!)+ 
+    qed (blast!)+
     thus "graph F f \<in> M" by (simp!)
   qed
   thus ?thesis
   proof
-    fix g assume "g \<in> M" "\<forall>x \<in> M. g \<subseteq> x --> g = x"
-    -- {* We consider such a maximal element $g \in M$. \skp *}
-    obtain H h where "graph H h = g" "is_linearform H h" 
-      "is_subspace H E" "is_subspace F H" "graph F f \<subseteq> graph H h" 
-      "\<forall>x \<in> H. h x <= p x" 
-      -- {* $g$ is a norm-preserving extension of $f$, in other words: *}
-      -- {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *}
-      -- {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *}
+    fix g assume "g \<in> M"  "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
+    -- {* We consider such a maximal element @{text "g \<in> M"}. \skp *}
+    obtain H h where "graph H h = g"  "is_linearform H h"
+      "is_subspace H E"  "is_subspace F H"  "graph F f \<subseteq> graph H h"
+      "\<forall>x \<in> H. h x \<le> p x"
+      -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *}
+      -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *}
+      -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *}
     proof -
-      have "\<exists>H h. graph H h = g \<and> is_linearform H h 
+      have "\<exists>H h. graph H h = g \<and> is_linearform H h
         \<and> is_subspace H E \<and> is_subspace F H
         \<and> graph F f \<subseteq> graph H h
-        \<and> (\<forall>x \<in> H. h x <= p x)" 
+        \<and> (\<forall>x \<in> H. h x \<le> p x)"
         by (simp! add: norm_pres_extension_D)
       with that show ?thesis by blast
     qed
     have h: "is_vectorspace H" ..
     have "H = E"
-    -- {* We show that $h$ is defined on whole $E$ by classical contradiction. \skp *} 
+    -- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *}
     proof (rule classical)
       assume "H \<noteq> E"
-      -- {* Assume $h$ is not defined on whole $E$. Then show that $h$ can be extended *}
-      -- {* in a norm-preserving way to a function $h'$ with the graph $g'$. \skp *}
+      -- {* Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended *}
+      -- {* in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp *}
       have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
       proof -
-        obtain x' where "x' \<in> E" "x' \<notin> H" 
-        -- {* Pick $x' \in E \setminus H$. \skp *}
+        obtain x' where "x' \<in> E"  "x' \<notin> H"
+        -- {* Pick @{text "x' \<in> E - H"}. \skp *}
         proof -
           have "\<exists>x' \<in> E. x' \<notin> H"
           proof (rule set_less_imp_diff_not_empty)
@@ -165,21 +155,21 @@
           with h have "x' \<in> H" by simp
           thus ?thesis by contradiction
         qed blast
-        def H' == "H + lin x'"
-        -- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}
-        obtain xi where "\<forall>y \<in> H. - p (y + x') - h y <= xi  
-                          \<and> xi <= p (y + x') - h y" 
-        -- {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
-        -- {* be used to establish that $h'$ is a norm-preserving extension of $h$. 
+        def H' \<equiv> "H + lin x'"
+        -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *}
+        obtain xi where "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
+                          \<and> xi \<le> p (y + x') - h y"
+        -- {* Pick a real number @{text \<xi>} that fulfills certain inequations; this will *}
+        -- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}.
            \label{ex-xi-use}\skp *}
         proof -
-          from h have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y <= xi 
-                          \<and> xi <= p (y + x') - h y" 
+          from h have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
+                          \<and> xi \<le> p (y + x') - h y"
           proof (rule ex_xi)
-            fix u v assume "u \<in> H" "v \<in> H"
+            fix u v assume "u \<in> H"  "v \<in> H"
             from h have "h v - h u = h (v - u)"
               by (simp! add: linearform_diff)
-            also have "... <= p (v - u)"
+            also have "... \<le> p (v - u)"
               by (simp!)
             also have "v - u = x' + - x' + v + - u"
               by (simp! add: diff_eq1)
@@ -187,29 +177,29 @@
               by (simp!)
             also have "... = (v + x') - (u + x')"
               by (simp! add: diff_eq1)
-            also have "p ... <= p (v + x') + p (u + x')"
+            also have "p ... \<le> p (v + x') + p (u + x')"
               by (rule seminorm_diff_subadditive) (simp_all!)
-            finally have "h v - h u <= p (v + x') + p (u + x')" .
+            finally have "h v - h u \<le> p (v + x') + p (u + x')" .
 
-            thus "- p (u + x') - h u <= p (v + x') - h v" 
+            thus "- p (u + x') - h u \<le> p (v + x') - h v"
               by (rule real_diff_ineq_swap)
           qed
           thus ?thesis ..
         qed
 
-        def h' == "\<lambda>x. let (y,a) = SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H
+        def h' \<equiv> "\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H
                        in h y + a * xi"
-        -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
+        -- {* Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \skp *}
         show ?thesis
         proof
-          show "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'" 
-          -- {* Show that $h'$ is an extension of $h$ \dots \skp *}
+          show "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
+          -- {* Show that @{text h'} is an extension of @{text h} \dots \skp *}
           proof
             show "g \<subseteq> graph H' h'"
             proof -
               have  "graph H h \<subseteq> graph H' h'"
               proof (rule graph_extI)
-                fix t assume "t \<in> H" 
+                fix t assume "t \<in> H"
                 have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H)
                      = (t, #0)"
                   by (rule decomp_H'_H) (assumption+, rule x')
@@ -223,7 +213,7 @@
                     show "is_vectorspace (lin x')" ..
                   qed
                 qed
-              qed 
+              qed
               thus ?thesis by (simp!)
             qed
             show "g \<noteq> graph H' h'"
@@ -231,7 +221,7 @@
               have "graph H h \<noteq> graph H' h'"
               proof
                 assume e: "graph H h = graph H' h'"
-                have "x' \<in> H'" 
+                have "x' \<in> H'"
                 proof (unfold H'_def, rule vs_sumI)
                   show "x' = 0 + x'" by (simp!)
                   from h show "0 \<in> H" ..
@@ -245,63 +235,63 @@
               thus ?thesis by (simp!)
             qed
           qed
-          show "graph H' h' \<in> M" 
-          -- {* and $h'$ is norm-preserving. \skp *}
+          show "graph H' h' \<in> M"
+          -- {* and @{text h'} is norm-preserving. \skp *}
           proof -
             have "graph H' h' \<in> norm_pres_extensions E p F f"
             proof (rule norm_pres_extensionI2)
               show "is_linearform H' h'"
                 by (rule h'_lf) (simp! add: x')+
-              show "is_subspace H' E" 
-                by (unfold H'_def) 
+              show "is_subspace H' E"
+                by (unfold H'_def)
                   (rule vs_sum_subspace [OF _ lin_subspace])
               have "is_subspace F H" .
-              also from h lin_vs 
+              also from h lin_vs
               have [folded H'_def]: "is_subspace H (H + lin x')" ..
-              finally (subspace_trans [OF _ h]) 
+              finally (subspace_trans [OF _ h])
               show f_h': "is_subspace F H'" .
-            
+
               show "graph F f \<subseteq> graph H' h'"
               proof (rule graph_extI)
                 fix x assume "x \<in> F"
                 have "f x = h x" ..
                 also have " ... = h x + #0 * xi" by simp
-                also 
-                have "... = (let (y,a) = (x, #0) in h y + a * xi)"
+                also
+                have "... = (let (y, a) = (x, #0) in h y + a * xi)"
                   by (simp add: Let_def)
-                also have 
+                also have
                   "(x, #0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
                   by (rule decomp_H'_H [symmetric]) (simp! add: x')+
-                also have 
-                  "(let (y,a) = (SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H)
+                also have
+                  "(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)
                     in h y + a * xi) = h' x" by (simp!)
                 finally show "f x = h' x" .
               next
                 from f_h' show "F \<subseteq> H'" ..
               qed
-            
-              show "\<forall>x \<in> H'. h' x <= p x"
+
+              show "\<forall>x \<in> H'. h' x \<le> p x"
                 by (rule h'_norm_pres) (assumption+, rule x')
             qed
             thus "graph H' h' \<in> M" by (simp!)
           qed
         qed
       qed
-      hence "\<not> (\<forall>x \<in> M. g \<subseteq> x --> g = x)" by simp
-	-- {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *}
+      hence "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
+        -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *}
       thus "H = E" by contradiction
     qed
-    thus "\<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x) 
-      \<and> (\<forall>x \<in> E. h x <= p x)" 
+    thus "\<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x)
+      \<and> (\<forall>x \<in> E. h x \<le> p x)"
     proof (intro exI conjI)
       assume eq: "H = E"
       from eq show "is_linearform E h" by (simp!)
       show "\<forall>x \<in> F. h x = f x"
       proof
-	fix x assume "x \<in> F" have "f x = h x " ..
-	thus "h x = f x" ..
+        fix x assume "x \<in> F" have "f x = h x " ..
+        thus "h x = f x" ..
       qed
-      from eq show "\<forall>x \<in> E. h x <= p x" by (force!)
+      from eq show "\<forall>x \<in> E. h x \<le> p x" by (blast!)
     qed
   qed
 qed
@@ -309,34 +299,37 @@
 
 subsection  {* Alternative formulation *}
 
-text {* The following alternative formulation of the Hahn-Banach
-Theorem\label{abs-HahnBanach} uses the fact that for a real linear form
-$f$ and a seminorm $p$ the
-following inequations are equivalent:\footnote{This was shown in lemma
-$\idt{abs{\dsh}ineq{\dsh}iff}$ (see page \pageref{abs-ineq-iff}).}
-\begin{matharray}{ll}
-\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\
-\forall x\in H.\ap h\ap x\leq p\ap x\\
-\end{matharray}
+text {*
+  The following alternative formulation of the Hahn-Banach
+  Theorem\label{abs-HahnBanach} uses the fact that for a real linear
+  form @{text f} and a seminorm @{text p} the following inequations
+  are equivalent:\footnote{This was shown in lemma @{thm [source]
+  abs_ineq_iff} (see page \pageref{abs-ineq-iff}).}
+  \begin{center}
+  \begin{tabular}{lll}
+  @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
+  @{text "\<forall>x \<in> H. h x \<le> p x"} \\
+  \end{tabular}
+  \end{center}
 *}
 
 theorem abs_HahnBanach:
-"[| is_vectorspace E; is_subspace F E; is_linearform F f; 
-is_seminorm E p; \<forall>x \<in> F. |f x| <= p x |]
-==> \<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
- \<and> (\<forall>x \<in> E. |g x| <= p x)"
+  "is_vectorspace E \<Longrightarrow> is_subspace F E \<Longrightarrow> is_linearform F f
+  \<Longrightarrow> is_seminorm E p \<Longrightarrow> \<forall>x \<in> F. \<bar>f x\<bar> \<le> p x
+  \<Longrightarrow> \<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
+    \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
 proof -
-assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
-"is_linearform F f"  "\<forall>x \<in> F. |f x| <= p x"
-have "\<forall>x \<in> F. f x <= p x"  by (rule abs_ineq_iff [THEN iffD1])
-hence "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x) 
-          \<and> (\<forall>x \<in> E. g x <= p x)"
+assume "is_vectorspace E"  "is_subspace F E"  "is_seminorm E p"
+"is_linearform F f"  "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
+have "\<forall>x \<in> F. f x \<le> p x"  by (rule abs_ineq_iff [THEN iffD1])
+hence "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
+          \<and> (\<forall>x \<in> E. g x \<le> p x)"
 by (simp! only: HahnBanach)
-thus ?thesis 
+thus ?thesis
 proof (elim exE conjE)
-fix g assume "is_linearform E g" "\<forall>x \<in> F. g x = f x" 
-              "\<forall>x \<in> E. g x <= p x"
-hence "\<forall>x \<in> E. |g x| <= p x"
+fix g assume "is_linearform E g"  "\<forall>x \<in> F. g x = f x"
+              "\<forall>x \<in> E. g x \<le> p x"
+hence "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
   by (simp! add: abs_ineq_iff [OF subspace_refl])
 thus ?thesis by (intro exI conjI)
 qed
@@ -344,170 +337,179 @@
 
 subsection {* The Hahn-Banach Theorem for normed spaces *}
 
-text {* Every continuous linear form $f$ on a subspace $F$ of a
-norm space $E$, can be extended to a continuous linear form $g$ on
-$E$ such that $\fnorm{f} = \fnorm {g}$. *}
+text {*
+  Every continuous linear form @{text f} on a subspace @{text F} of a
+  norm space @{text E}, can be extended to a continuous linear form
+  @{text g} on @{text E} such that @{text "\<parallel>f\<parallel> = \<parallel>g\<parallel>"}.
+*}
 
 theorem norm_HahnBanach:
-"[| is_normed_vectorspace E norm; is_subspace F E; 
-is_linearform F f; is_continuous F norm f |] 
-==> \<exists>g. is_linearform E g
-     \<and> is_continuous E norm g 
-     \<and> (\<forall>x \<in> F. g x = f x) 
+  "is_normed_vectorspace E norm \<Longrightarrow> is_subspace F E
+  \<Longrightarrow> is_linearform F f \<Longrightarrow> is_continuous F norm f
+  \<Longrightarrow> \<exists>g. is_linearform E g
+     \<and> is_continuous E norm g
+     \<and> (\<forall>x \<in> F. g x = f x)
      \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
 proof -
 assume e_norm: "is_normed_vectorspace E norm"
-assume f: "is_subspace F E" "is_linearform F f"
+assume f: "is_subspace F E"  "is_linearform F f"
 assume f_cont: "is_continuous F norm f"
 have e: "is_vectorspace E" ..
 hence f_norm: "is_normed_vectorspace F norm" ..
 
-txt{* We define a function $p$ on $E$ as follows:
-\begin{matharray}{l}
-p \: x = \fnorm f \cdot \norm x\\
-\end{matharray}
+txt{*
+  We define a function @{text p} on @{text E} as follows:
+  @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
 *}
 
-def p == "\<lambda>x. \<parallel>f\<parallel>F,norm * norm x"
+def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>F,norm * norm x"
 
-txt{* $p$ is a seminorm on $E$: *}
+txt {* @{text p} is a seminorm on @{text E}: *}
 
 have q: "is_seminorm E p"
 proof
-fix x y a assume "x \<in> E" "y \<in> E"
+fix x y a assume "x \<in> E"  "y \<in> E"
 
-txt{* $p$ is positive definite: *}
+txt {* @{text p} is positive definite: *}
 
-show "#0 <= p x"
+show "#0 \<le> p x"
 proof (unfold p_def, rule real_le_mult_order1a)
-  from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
-  show "#0 <= norm x" ..
+  from f_cont f_norm show "#0 \<le> \<parallel>f\<parallel>F,norm" ..
+  show "#0 \<le> norm x" ..
 qed
 
-txt{* $p$ is absolutely homogenous: *}
+txt {* @{text p} is absolutely homogenous: *}
 
-show "p (a \<cdot> x) = |a| * p x"
-proof - 
+show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
+proof -
   have "p (a \<cdot> x) = \<parallel>f\<parallel>F,norm * norm (a \<cdot> x)"
     by (simp!)
-  also have "norm (a \<cdot> x) = |a| * norm x" 
+  also have "norm (a \<cdot> x) = \<bar>a\<bar> * norm x"
     by (rule normed_vs_norm_abs_homogenous)
-  also have "\<parallel>f\<parallel>F,norm * ( |a| * norm x ) 
-    = |a| * (\<parallel>f\<parallel>F,norm * norm x)"
+  also have "\<parallel>f\<parallel>F,norm * (\<bar>a\<bar> * norm x )
+    = \<bar>a\<bar> * (\<parallel>f\<parallel>F,norm * norm x)"
     by (simp! only: real_mult_left_commute)
-  also have "... = |a| * p x" by (simp!)
+  also have "... = \<bar>a\<bar> * p x" by (simp!)
   finally show ?thesis .
 qed
 
-txt{* Furthermore, $p$ is subadditive: *}
+txt {* Furthermore, @{text p} is subadditive: *}
 
-show "p (x + y) <= p x + p y"
+show "p (x + y) \<le> p x + p y"
 proof -
   have "p (x + y) = \<parallel>f\<parallel>F,norm * norm (x + y)"
     by (simp!)
-  also 
-  have "... <= \<parallel>f\<parallel>F,norm * (norm x + norm y)"
+  also
+  have "... \<le> \<parallel>f\<parallel>F,norm * (norm x + norm y)"
   proof (rule real_mult_le_le_mono1a)
-    from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
-    show "norm (x + y) <= norm x + norm y" ..
+    from f_cont f_norm show "#0 \<le> \<parallel>f\<parallel>F,norm" ..
+    show "norm (x + y) \<le> norm x + norm y" ..
   qed
-  also have "... = \<parallel>f\<parallel>F,norm * norm x 
+  also have "... = \<parallel>f\<parallel>F,norm * norm x
                     + \<parallel>f\<parallel>F,norm * norm y"
     by (simp! only: real_add_mult_distrib2)
   finally show ?thesis by (simp!)
 qed
 qed
 
-txt{* $f$ is bounded by $p$. *} 
+txt {* @{text f} is bounded by @{text p}. *}
 
-have "\<forall>x \<in> F. |f x| <= p x"
+have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
 proof
 fix x assume "x \<in> F"
- from f_norm show "|f x| <= p x" 
+ from f_norm show "\<bar>f x\<bar> \<le> p x"
    by (simp! add: norm_fx_le_norm_f_norm_x)
 qed
 
-txt{* Using the fact that $p$ is a seminorm and 
-$f$ is bounded by $p$ we can apply the Hahn-Banach Theorem 
-for real vector spaces. 
-So $f$ can be extended in a norm-preserving way to some function
-$g$ on the whole vector space $E$. *}
+txt {*
+  Using the fact that @{text p} is a seminorm and @{text f} is bounded
+  by @{text p} we can apply the Hahn-Banach Theorem for real vector
+  spaces. So @{text f} can be extended in a norm-preserving way to
+  some function @{text g} on the whole vector space @{text E}.
+*}
 
-with e f q 
-have "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x) 
-        \<and> (\<forall>x \<in> E. |g x| <= p x)"
+with e f q
+have "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
+        \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
 by (simp! add: abs_HahnBanach)
 
 thus ?thesis
-proof (elim exE conjE) 
+proof (elim exE conjE)
 fix g
-assume "is_linearform E g" and a: "\<forall>x \<in> F. g x = f x" 
-   and b: "\<forall>x \<in> E. |g x| <= p x"
+assume "is_linearform E g" and a: "\<forall>x \<in> F. g x = f x"
+   and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
 
-show "\<exists>g. is_linearform E g 
-        \<and> is_continuous E norm g 
-        \<and> (\<forall>x \<in> F. g x = f x) 
+show "\<exists>g. is_linearform E g
+        \<and> is_continuous E norm g
+        \<and> (\<forall>x \<in> F. g x = f x)
         \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
 proof (intro exI conjI)
 
-txt{* We furthermore have to show that 
-$g$ is also continuous: *}
+txt {*
+  We furthermore have to show that @{text g} is also continuous:
+*}
 
   show g_cont: "is_continuous E norm g"
   proof
     fix x assume "x \<in> E"
-    with b show "|g x| <= \<parallel>f\<parallel>F,norm * norm x"
-      by (simp add: p_def) 
-  qed 
+    with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>F,norm * norm x"
+      by (simp add: p_def)
+  qed
 
-  txt {* To complete the proof, we show that 
-  $\fnorm g = \fnorm f$. \label{order_antisym} *}
+  txt {*
+    To complete the proof, we show that
+    @{text "\<parallel>g\<parallel> = \<parallel>f\<parallel>"}. \label{order_antisym} *}
 
   show "\<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
     (is "?L = ?R")
   proof (rule order_antisym)
 
-    txt{* First we show $\fnorm g \leq \fnorm f$.  The function norm
-    $\fnorm g$ is defined as the smallest $c\in\bbbR$ such that
-    \begin{matharray}{l}
-    \All {x\in E} {|g\ap x| \leq c \cdot \norm x}
-    \end{matharray}
-    Furthermore holds
-    \begin{matharray}{l}
-    \All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x}
-    \end{matharray}
+    txt {*
+      First we show @{text "\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>"}.  The function norm @{text
+      "\<parallel>g\<parallel>"} is defined as the smallest @{text "c \<in> \<real>"} such that
+      \begin{center}
+      \begin{tabular}{l}
+      @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+      \end{tabular}
+      \end{center}
+      \noindent Furthermore holds
+      \begin{center}
+      \begin{tabular}{l}
+      @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+      \end{tabular}
+      \end{center}
     *}
- 
-    have "\<forall>x \<in> E. |g x| <= \<parallel>f\<parallel>F,norm * norm x"
+
+    have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel>F,norm * norm x"
     proof
-      fix x assume "x \<in> E" 
-      show "|g x| <= \<parallel>f\<parallel>F,norm * norm x"
+      fix x assume "x \<in> E"
+      show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>F,norm * norm x"
         by (simp!)
     qed
 
-    with g_cont e_norm show "?L <= ?R"
+    with g_cont e_norm show "?L \<le> ?R"
     proof (rule fnorm_le_ub)
-      from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
+      from f_cont f_norm show "#0 \<le> \<parallel>f\<parallel>F,norm" ..
     qed
 
-    txt{* The other direction is achieved by a similar 
+    txt{* The other direction is achieved by a similar
     argument. *}
 
-    have "\<forall>x \<in> F. |f x| <= \<parallel>g\<parallel>E,norm * norm x"
+    have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>E,norm * norm x"
     proof
-      fix x assume "x \<in> F" 
+      fix x assume "x \<in> F"
       from a have "g x = f x" ..
-      hence "|f x| = |g x|" by simp
+      hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by simp
       also from g_cont
-      have "... <= \<parallel>g\<parallel>E,norm * norm x"
+      have "... \<le> \<parallel>g\<parallel>E,norm * norm x"
       proof (rule norm_fx_le_norm_f_norm_x)
         show "x \<in> E" ..
       qed
-      finally show "|f x| <= \<parallel>g\<parallel>E,norm * norm x" .
-    qed 
-    thus "?R <= ?L" 
+      finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>E,norm * norm x" .
+    qed
+    thus "?R \<le> ?L"
     proof (rule fnorm_le_ub [OF f_cont f_norm])
-      from g_cont show "#0 <= \<parallel>g\<parallel>E,norm" ..
+      from g_cont show "#0 \<le> \<parallel>g\<parallel>E,norm" ..
     qed
   qed
 qed
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -7,155 +7,162 @@
 
 theory HahnBanachExtLemmas = FunctionNorm:
 
-text{* In this section the following context is presumed.
-Let $E$ be a real vector space with a 
-seminorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear 
-function on $F$. We consider a subspace $H$ of $E$ that is a 
-superspace of $F$ and a linear form $h$ on $H$. $H$ is a not equal 
-to $E$ and $x_0$ is an element in $E \backslash H$.
-$H$ is extended to the direct sum  $H' = H + \idt{lin}\ap x_0$, so for
-any $x\in H'$ the decomposition of $x = y + a \mult x$ 
-with $y\in H$ is unique. $h'$ is defined on $H'$ by  
-$h'\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$.
+text {*
+  In this section the following context is presumed.  Let @{text E} be
+  a real vector space with a seminorm @{text q} on @{text E}. @{text
+  F} is a subspace of @{text E} and @{text f} a linear function on
+  @{text F}. We consider a subspace @{text H} of @{text E} that is a
+  superspace of @{text F} and a linear form @{text h} on @{text
+  H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is
+  an element in @{text "E - H"}.  @{text H} is extended to the direct
+  sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"}
+  the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is
+  unique. @{text h'} is defined on @{text H'} by
+  @{text "h' x = h y + a \<cdot> \<xi>"} for a certain @{text \<xi>}.
 
-Subsequently we show some properties of this extension $h'$ of $h$.
-*} 
-
+  Subsequently we show some properties of this extension @{text h'} of
+  @{text h}.
+*}
 
-text {* This lemma will be used to show the existence of a linear
-extension of $f$ (see page \pageref{ex-xi-use}). 
-It is a consequence
-of the completeness of $\bbbR$. To show 
-\begin{matharray}{l}
-\Ex{\xi}{\All {y\in F}{a\ap y \leq \xi \land \xi \leq b\ap y}}
-\end{matharray} 
-it suffices to show that 
-\begin{matharray}{l} \All
-{u\in F}{\All {v\in F}{a\ap u \leq b \ap v}} 
-\end{matharray} *}
+text {*
+  This lemma will be used to show the existence of a linear extension
+  of @{text f} (see page \pageref{ex-xi-use}). It is a consequence of
+  the completeness of @{text \<real>}. To show
+  \begin{center}
+  \begin{tabular}{l}
+  @{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"}
+  \end{tabular}
+  \end{center}
+  \noindent it suffices to show that
+  \begin{center}
+  \begin{tabular}{l}
+  @{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}
+  \end{tabular}
+  \end{center}
+*}
 
-lemma ex_xi: 
-  "[| is_vectorspace F; !! u v. [| u \<in> F; v \<in> F |] ==> a u <= b v |]
-  ==> \<exists>xi::real. \<forall>y \<in> F. a y <= xi \<and> xi <= b y" 
+lemma ex_xi:
+  "is_vectorspace F \<Longrightarrow> (\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v)
+  \<Longrightarrow> \<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
 proof -
   assume vs: "is_vectorspace F"
-  assume r: "(!! u v. [| u \<in> F; v \<in> F |] ==> a u <= (b v::real))"
+  assume r: "(\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> (b v::real))"
 
   txt {* From the completeness of the reals follows:
-  The set $S = \{a\: u\dt\: u\in F\}$ has a supremum, if
+  The set @{text "S = {a u. u \<in> F}"} has a supremum, if
   it is non-empty and has an upper bound. *}
 
   let ?S = "{a u :: real | u. u \<in> F}"
 
-  have "\<exists>xi. isLub UNIV ?S xi"  
+  have "\<exists>xi. isLub UNIV ?S xi"
   proof (rule reals_complete)
-  
-    txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *}
 
-    from vs have "a 0 \<in> ?S" by force
+    txt {* The set @{text S} is non-empty, since @{text "a 0 \<in> S"}: *}
+
+    from vs have "a 0 \<in> ?S" by blast
     thus "\<exists>X. X \<in> ?S" ..
 
-    txt {* $b\ap \zero$ is an upper bound of $S$: *}
+    txt {* @{text "b 0"} is an upper bound of @{text S}: *}
 
-    show "\<exists>Y. isUb UNIV ?S Y" 
-    proof 
+    show "\<exists>Y. isUb UNIV ?S Y"
+    proof
       show "isUb UNIV ?S (b 0)"
       proof (intro isUbI setleI ballI)
         show "b 0 \<in> UNIV" ..
       next
 
-        txt {* Every element $y\in S$ is less than $b\ap \zero$: *}
+        txt {* Every element @{text "y \<in> S"} is less than @{text "b 0"}: *}
 
-        fix y assume y: "y \<in> ?S" 
+        fix y assume y: "y \<in> ?S"
         from y have "\<exists>u \<in> F. y = a u" by fast
-        thus "y <= b 0" 
+        thus "y \<le> b 0"
         proof
-          fix u assume "u \<in> F" 
+          fix u assume "u \<in> F"
           assume "y = a u"
-          also have "a u <= b 0" by (rule r) (simp!)+
+          also have "a u \<le> b 0" by (rule r) (simp!)+
           finally show ?thesis .
         qed
       qed
     qed
   qed
 
-  thus "\<exists>xi. \<forall>y \<in> F. a y <= xi \<and> xi <= b y" 
+  thus "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
   proof (elim exE)
-    fix xi assume "isLub UNIV ?S xi" 
+    fix xi assume "isLub UNIV ?S xi"
     show ?thesis
-    proof (intro exI conjI ballI) 
-   
-      txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *}
-     
+    proof (intro exI conjI ballI)
+
+      txt {* For all @{text "y \<in> F"} holds @{text "a y \<le> \<xi>"}: *}
+
       fix y assume y: "y \<in> F"
-      show "a y <= xi"    
-      proof (rule isUbD)  
+      show "a y \<le> xi"
+      proof (rule isUbD)
         show "isUb UNIV ?S xi" ..
-      qed (force!)
+      qed (blast!)
     next
 
-      txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *}
+      txt {* For all @{text "y \<in> F"} holds @{text "\<xi> \<le> b y"}: *}
 
       fix y assume "y \<in> F"
-      show "xi <= b y"  
+      show "xi \<le> b y"
       proof (intro isLub_le_isUb isUbI setleI)
         show "b y \<in> UNIV" ..
-        show "\<forall>ya \<in> ?S. ya <= b y" 
+        show "\<forall>ya \<in> ?S. ya \<le> b y"
         proof
           fix au assume au: "au \<in> ?S "
           hence "\<exists>u \<in> F. au = a u" by fast
-          thus "au <= b y"
+          thus "au \<le> b y"
           proof
-            fix u assume "u \<in> F" assume "au = a u"  
-            also have "... <= b y" by (rule r)
+            fix u assume "u \<in> F" assume "au = a u"
+            also have "... \<le> b y" by (rule r)
             finally show ?thesis .
           qed
         qed
-      qed 
+      qed
     qed
   qed
 qed
 
-text{* \medskip The function $h'$ is defined as a
-$h'\ap x = h\ap y + a\cdot \xi$ where $x = y + a\mult \xi$
-is a linear extension of $h$ to $H'$. *}
+text {*
+  \medskip The function @{text h'} is defined as a
+  @{text "h' x = h y + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a
+  linear extension of @{text h} to @{text H'}. *}
 
-lemma h'_lf: 
-  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
-                in h y + a * xi);
-  H' == H + lin x0; is_subspace H E; is_linearform H h; x0 \<notin> H; 
-  x0 \<in> E; x0 \<noteq> 0; is_vectorspace E |]
-  ==> is_linearform H' h'"
+lemma h'_lf:
+  "h' \<equiv> \<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi
+  \<Longrightarrow> H' \<equiv> H + lin x0 \<Longrightarrow> is_subspace H E \<Longrightarrow> is_linearform H h \<Longrightarrow> x0 \<notin> H
+  \<Longrightarrow> x0 \<in> E \<Longrightarrow> x0 \<noteq> 0 \<Longrightarrow> is_vectorspace E
+  \<Longrightarrow> is_linearform H' h'"
 proof -
-  assume h'_def: 
-    "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
+  assume h'_def:
+    "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
                in h y + a * xi)"
-    and H'_def: "H' == H + lin x0" 
-    and vs: "is_subspace H E" "is_linearform H h" "x0 \<notin> H"
-      "x0 \<noteq> 0" "x0 \<in> E" "is_vectorspace E"
+    and H'_def: "H' \<equiv> H + lin x0"
+    and vs: "is_subspace H E"  "is_linearform H h"  "x0 \<notin> H"
+      "x0 \<noteq> 0"  "x0 \<in> E"  "is_vectorspace E"
 
-  have h': "is_vectorspace H'" 
+  have h': "is_vectorspace H'"
   proof (unfold H'_def, rule vs_sum_vs)
     show "is_subspace (lin x0) E" ..
-  qed 
+  qed
 
   show ?thesis
   proof
-    fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'" 
+    fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
 
-    txt{* We now have to show that $h'$ is additive, i.~e.\
-    $h' \ap (x_1\plus x_2) = h'\ap x_1 + h'\ap x_2$
-    for $x_1, x_2\in H$. *} 
+    txt {* We now have to show that @{text h'} is additive, i.~e.\
+      @{text "h' (x\<^sub>1 + x\<^sub>2) = h' x\<^sub>1 + h' x\<^sub>2"} for
+      @{text "x\<^sub>1, x\<^sub>2 \<in> H"}. *}
 
-    have x1x2: "x1 + x2 \<in> H'" 
-      by (rule vs_add_closed, rule h') 
-    from x1 
-    have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0  \<and> y1 \<in> H" 
+    have x1x2: "x1 + x2 \<in> H'"
+      by (rule vs_add_closed, rule h')
+    from x1
+    have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0  \<and> y1 \<in> H"
       by (unfold H'_def vs_sum_def lin_def) fast
-    from x2 
-    have ex_x2: "\<exists>y2 a2. x2 = y2 + a2 \<cdot> x0 \<and> y2 \<in> H" 
+    from x2
+    have ex_x2: "\<exists>y2 a2. x2 = y2 + a2 \<cdot> x0 \<and> y2 \<in> H"
       by (unfold H'_def vs_sum_def lin_def) fast
-    from x1x2 
+    from x1x2
     have ex_x1x2: "\<exists>y a. x1 + x2 = y + a \<cdot> x0 \<and> y \<in> H"
       by (unfold H'_def vs_sum_def lin_def) fast
 
@@ -164,181 +171,178 @@
     proof (elim exE conjE)
       fix y1 y2 y a1 a2 a
       assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
-         and y2: "x2 = y2 + a2 \<cdot> x0"     and y2': "y2 \<in> H" 
-         and y: "x1 + x2 = y + a \<cdot> x0"   and y':  "y  \<in> H" 
+         and y2: "x2 = y2 + a2 \<cdot> x0"     and y2': "y2 \<in> H"
+         and y: "x1 + x2 = y + a \<cdot> x0"   and y':  "y  \<in> H"
       txt {* \label{decomp-H-use}*}
-      have ya: "y1 + y2 = y \<and> a1 + a2 = a" 
+      have ya: "y1 + y2 = y \<and> a1 + a2 = a"
       proof (rule decomp_H')
-        show "y1 + y2 + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" 
+        show "y1 + y2 + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0"
           by (simp! add: vs_add_mult_distrib2 [of E])
         show "y1 + y2 \<in> H" ..
       qed
 
       have "h' (x1 + x2) = h y + a * xi"
-	by (rule h'_definite)
-      also have "... = h (y1 + y2) + (a1 + a2) * xi" 
+        by (rule h'_definite)
+      also have "... = h (y1 + y2) + (a1 + a2) * xi"
         by (simp add: ya)
-      also from vs y1' y2' 
-      have "... = h y1 + h y2 + a1 * xi + a2 * xi" 
-	by (simp add: linearform_add [of H] 
+      also from vs y1' y2'
+      have "... = h y1 + h y2 + a1 * xi + a2 * xi"
+        by (simp add: linearform_add [of H]
                       real_add_mult_distrib)
-      also have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)" 
+      also have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
         by simp
       also have "h y1 + a1 * xi = h' x1"
         by (rule h'_definite [symmetric])
-      also have "h y2 + a2 * xi = h' x2" 
+      also have "h y2 + a2 * xi = h' x2"
         by (rule h'_definite [symmetric])
       finally show ?thesis .
     qed
- 
-    txt{* We further have to show that $h'$ is multiplicative, 
-    i.~e.\ $h'\ap (c \mult x_1) = c \cdot h'\ap x_1$
-    for $x\in H$ and $c\in \bbbR$. 
-    *} 
 
-  next  
-    fix c x1 assume x1: "x1 \<in> H'"    
+    txt {* We further have to show that @{text h'} is multiplicative,
+    i.~e.\ @{text "h' (c \<cdot> x\<^sub>1) = c \<cdot> h' x\<^sub>1"} for @{text "x \<in> H"}
+    and @{text "c \<in> \<real>"}. *}
+
+  next
+    fix c x1 assume x1: "x1 \<in> H'"
     have ax1: "c \<cdot> x1 \<in> H'"
       by (rule vs_mult_closed, rule h')
-    from x1 
-    have ex_x: "!! x. x\<in> H' ==> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
+    from x1
+    have ex_x: "\<And>x. x\<in> H' \<Longrightarrow> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
       by (unfold H'_def vs_sum_def lin_def) fast
 
     from x1 have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H"
       by (unfold H'_def vs_sum_def lin_def) fast
     with ex_x [of "c \<cdot> x1", OF ax1]
-    show "h' (c \<cdot> x1) = c * (h' x1)"  
+    show "h' (c \<cdot> x1) = c * (h' x1)"
     proof (elim exE conjE)
-      fix y1 y a1 a 
+      fix y1 y a1 a
       assume y1: "x1 = y1 + a1 \<cdot> x0"     and y1': "y1 \<in> H"
-        and y: "c \<cdot> x1 = y  + a \<cdot> x0"    and y': "y \<in> H" 
+        and y: "c \<cdot> x1 = y  + a \<cdot> x0"    and y': "y \<in> H"
 
-      have ya: "c \<cdot> y1 = y \<and> c * a1 = a" 
-      proof (rule decomp_H') 
-	show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" 
+      have ya: "c \<cdot> y1 = y \<and> c * a1 = a"
+      proof (rule decomp_H')
+        show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0"
           by (simp! add: vs_add_mult_distrib1)
         show "c \<cdot> y1 \<in> H" ..
       qed
 
-      have "h' (c \<cdot> x1) = h y + a * xi" 
-	by (rule h'_definite)
+      have "h' (c \<cdot> x1) = h y + a * xi"
+        by (rule h'_definite)
       also have "... = h (c \<cdot> y1) + (c * a1) * xi"
         by (simp add: ya)
-      also from vs y1' have "... = c * h y1 + c * a1 * xi" 
-	by (simp add: linearform_mult [of H])
-      also from vs y1' have "... = c * (h y1 + a1 * xi)" 
-	by (simp add: real_add_mult_distrib2 real_mult_assoc)
-      also have "h y1 + a1 * xi = h' x1" 
+      also from vs y1' have "... = c * h y1 + c * a1 * xi"
+        by (simp add: linearform_mult [of H])
+      also from vs y1' have "... = c * (h y1 + a1 * xi)"
+        by (simp add: real_add_mult_distrib2 real_mult_assoc)
+      also have "h y1 + a1 * xi = h' x1"
         by (rule h'_definite [symmetric])
       finally show ?thesis .
     qed
   qed
 qed
 
-text{* \medskip The linear extension $h'$ of $h$
-is bounded by the seminorm $p$. *}
+text {* \medskip The linear extension @{text h'} of @{text h}
+is bounded by the seminorm @{text p}. *}
 
 lemma h'_norm_pres:
-  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
-                 in h y + a * xi);
-  H' == H + lin x0; x0 \<notin> H; x0 \<in> E; x0 \<noteq> 0; is_vectorspace E; 
-  is_subspace H E; is_seminorm E p; is_linearform H h; 
-  \<forall>y \<in> H. h y <= p y; 
-  \<forall>y \<in> H. - p (y + x0) - h y <= xi \<and> xi <= p (y + x0) - h y |]
-   ==> \<forall>x \<in> H'. h' x <= p x" 
-proof 
-  assume h'_def: 
-    "h' == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H 
+  "h' \<equiv> \<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi
+  \<Longrightarrow> H' \<equiv> H + lin x0 \<Longrightarrow> x0 \<notin> H \<Longrightarrow> x0 \<in> E \<Longrightarrow> x0 \<noteq> 0 \<Longrightarrow> is_vectorspace E
+  \<Longrightarrow> is_subspace H E \<Longrightarrow> is_seminorm E p \<Longrightarrow> is_linearform H h
+  \<Longrightarrow> \<forall>y \<in> H. h y \<le> p y
+  \<Longrightarrow> \<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y
+  \<Longrightarrow> \<forall>x \<in> H'. h' x \<le> p x"
+proof
+  assume h'_def:
+    "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
                in (h y) + a * xi)"
-    and H'_def: "H' == H + lin x0" 
-    and vs: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" "is_vectorspace E" 
-            "is_subspace H E" "is_seminorm E p" "is_linearform H h" 
-    and a: "\<forall>y \<in> H. h y <= p y"
-  presume a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya <= xi"
-  presume a2: "\<forall>ya \<in> H. xi <= p (ya + x0) - h ya"
-  fix x assume "x \<in> H'" 
-  have ex_x: 
-    "!! x. x \<in> H' ==> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
+    and H'_def: "H' \<equiv> H + lin x0"
+    and vs: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"  "is_vectorspace E"
+            "is_subspace H E"  "is_seminorm E p"  "is_linearform H h"
+    and a: "\<forall>y \<in> H. h y \<le> p y"
+  presume a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
+  presume a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya"
+  fix x assume "x \<in> H'"
+  have ex_x:
+    "\<And>x. x \<in> H' \<Longrightarrow> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
     by (unfold H'_def vs_sum_def lin_def) fast
   have "\<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
     by (rule ex_x)
-  thus "h' x <= p x"
+  thus "h' x \<le> p x"
   proof (elim exE conjE)
     fix y a assume x: "x = y + a \<cdot> x0" and y: "y \<in> H"
     have "h' x = h y + a * xi"
       by (rule h'_definite)
 
-    txt{* Now we show  
-    $h\ap y + a \cdot \xi\leq  p\ap (y\plus a \mult x_0)$ 
-    by case analysis on $a$. *}
+    txt {* Now we show @{text "h y + a \<cdot> \<xi> \<le> p (y + a \<cdot> x\<^sub>0)"}
+    by case analysis on @{text a}. *}
 
-    also have "... <= p (y + a \<cdot> x0)"
+    also have "... \<le> p (y + a \<cdot> x0)"
     proof (rule linorder_cases)
 
-      assume z: "a = #0" 
+      assume z: "a = #0"
       with vs y a show ?thesis by simp
 
-    txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$ 
-    taken as $y/a$: *}
+    txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
+    with @{text ya} taken as @{text "y / a"}: *}
 
     next
       assume lz: "a < #0" hence nz: "a \<noteq> #0" by simp
-      from a1 
-      have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) <= xi"
+      from a1
+      have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi"
         by (rule bspec) (simp!)
 
-      txt {* The thesis for this case now follows by a short  
-      calculation. *}      
-      hence "a * xi <= a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
+      txt {* The thesis for this case now follows by a short
+      calculation. *}
+      hence "a * xi \<le> a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
         by (rule real_mult_less_le_anti [OF lz])
-      also 
+      also
       have "... = - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
         by (rule real_mult_diff_distrib)
-      also from lz vs y 
+      also from lz vs y
       have "- a * (p (inverse a \<cdot> y + x0)) = p (a \<cdot> (inverse a \<cdot> y + x0))"
         by (simp add: seminorm_abs_homogenous abs_minus_eqI2)
       also from nz vs y have "... = p (y + a \<cdot> x0)"
         by (simp add: vs_add_mult_distrib1)
       also from nz vs y have "a * (h (inverse a \<cdot> y)) =  h y"
         by (simp add: linearform_mult [symmetric])
-      finally have "a * xi <= p (y + a \<cdot> x0) - h y" .
+      finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
 
-      hence "h y + a * xi <= h y + p (y + a \<cdot> x0) - h y"
+      hence "h y + a * xi \<le> h y + p (y + a \<cdot> x0) - h y"
         by (simp add: real_add_left_cancel_le)
       thus ?thesis by simp
 
-      txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$ 
-      taken as $y/a$: *}
+      txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
+        with @{text ya} taken as @{text "y / a"}: *}
 
-    next 
+    next
       assume gz: "#0 < a" hence nz: "a \<noteq> #0" by simp
-      from a2 have "xi <= p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)"
+      from a2 have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)"
         by (rule bspec) (simp!)
 
       txt {* The thesis for this case follows by a short
       calculation: *}
 
-      with gz 
-      have "a * xi <= a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
+      with gz
+      have "a * xi \<le> a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
         by (rule real_mult_less_le_mono)
       also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
-        by (rule real_mult_diff_distrib2) 
-      also from gz vs y 
+        by (rule real_mult_diff_distrib2)
+      also from gz vs y
       have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
         by (simp add: seminorm_abs_homogenous abs_eqI2)
       also from nz vs y have "... = p (y + a \<cdot> x0)"
         by (simp add: vs_add_mult_distrib1)
       also from nz vs y have "a * h (inverse a \<cdot> y) = h y"
-        by (simp add: linearform_mult [symmetric]) 
-      finally have "a * xi <= p (y + a \<cdot> x0) - h y" .
- 
-      hence "h y + a * xi <= h y + (p (y + a \<cdot> x0) - h y)"
+        by (simp add: linearform_mult [symmetric])
+      finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
+
+      hence "h y + a * xi \<le> h y + (p (y + a \<cdot> x0) - h y)"
         by (simp add: real_add_left_cancel_le)
       thus ?thesis by simp
     qed
     also from x have "... = p x" by simp
     finally show ?thesis .
   qed
-qed blast+ 
+qed blast+
 
 end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/HahnBanachLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachLemmas.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachLemmas.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -1,3 +1,4 @@
-
+(*<*)
 theory HahnBanachLemmas = HahnBanachSupLemmas + HahnBanachExtLemmas:
 end
+(*>*)
\ No newline at end of file
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -7,57 +7,59 @@
 
 theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:
 
-text{* This section contains some lemmas that will be used in the
-proof of the Hahn-Banach Theorem.
-In this section the following context is presumed. 
-Let $E$ be a real vector space with a seminorm $p$ on $E$. 
-$F$ is a subspace of $E$ and $f$ a linear form on $F$. We 
-consider a chain $c$ of norm-preserving extensions of $f$, such that
-$\Union c = \idt{graph}\ap H\ap h$. 
-We will show some properties about the limit function $h$, 
-i.e.\ the supremum of the chain $c$.
-*} 
+text {*
+  This section contains some lemmas that will be used in the proof of
+  the Hahn-Banach Theorem.  In this section the following context is
+  presumed.  Let @{text E} be a real vector space with a seminorm
+  @{text p} on @{text E}.  @{text F} is a subspace of @{text E} and
+  @{text f} a linear form on @{text F}. We consider a chain @{text c}
+  of norm-preserving extensions of @{text f}, such that
+  @{text "\<Union>c = graph H h"}.  We will show some properties about the
+  limit function @{text h}, i.e.\ the supremum of the chain @{text c}.
+*}
 
-text{* Let $c$ be a chain of norm-preserving extensions of the 
-function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$. 
-Every element in $H$ is member of
-one of the elements of the chain. *}
+text {*
+  Let @{text c} be a chain of norm-preserving extensions of the
+  function @{text f} and let @{text "graph H h"} be the supremum of
+  @{text c}.  Every element in @{text H} is member of one of the
+  elements of the chain.
+*}
 
 lemma some_H'h't:
-  "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
-  graph H h = \<Union>c; x \<in> H |]
-   ==> \<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h' 
-       \<and> is_linearform H' h' \<and> is_subspace H' E 
-       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
-       \<and> (\<forall>x \<in> H'. h' x <= p x)"
+  "M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
+  graph H h = \<Union>c \<Longrightarrow> x \<in> H
+   \<Longrightarrow> \<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
+       \<and> is_linearform H' h' \<and> is_subspace H' E
+       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+       \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
 proof -
   assume m: "M = norm_pres_extensions E p F f" and "c \<in> chain M"
-     and u: "graph H h = \<Union>c" "x \<in> H"
+     and u: "graph H h = \<Union>c"  "x \<in> H"
 
   have h: "(x, h x) \<in> graph H h" ..
   with u have "(x, h x) \<in> \<Union>c" by simp
-  hence ex1: "\<exists>g \<in> c. (x, h x) \<in> g" 
+  hence ex1: "\<exists>g \<in> c. (x, h x) \<in> g"
     by (simp only: Union_iff)
   thus ?thesis
   proof (elim bexE)
-    fix g assume g: "g \<in> c" "(x, h x) \<in> g"
+    fix g assume g: "g \<in> c"  "(x, h x) \<in> g"
     have "c \<subseteq> M" by (rule chainD2)
     hence "g \<in> M" ..
     hence "g \<in> norm_pres_extensions E p F f" by (simp only: m)
-    hence "\<exists>H' h'. graph H' h' = g 
+    hence "\<exists>H' h'. graph H' h' = g
                   \<and> is_linearform H' h'
                   \<and> is_subspace H' E
                   \<and> is_subspace F H'
                   \<and> graph F f \<subseteq> graph H' h'
-                  \<and> (\<forall>x \<in> H'. h' x <= p x)"
+                  \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
       by (rule norm_pres_extension_D)
     thus ?thesis
-    proof (elim exE conjE) 
-      fix H' h' 
-      assume "graph H' h' = g" "is_linearform H' h'" 
-        "is_subspace H' E" "is_subspace F H'" 
-        "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x <= p x"
-      show ?thesis 
+    proof (elim exE conjE)
+      fix H' h'
+      assume "graph H' h' = g"  "is_linearform H' h'"
+        "is_subspace H' E"  "is_subspace F H'"
+        "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
+      show ?thesis
       proof (intro exI conjI)
         show "graph H' h' \<in> c" by (simp!)
         show "(x, h x) \<in> graph H' h'" by (simp!)
@@ -67,93 +69,99 @@
 qed
 
 
-text{*  \medskip Let $c$ be a chain of norm-preserving extensions of the
-function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$. 
-Every element in the domain $H$ of the supremum function is member of
-the domain $H'$ of some function $h'$, such that $h$ extends $h'$.
+text {*
+  \medskip Let @{text c} be a chain of norm-preserving extensions of
+  the function @{text f} and let @{text "graph H h"} be the supremum
+  of @{text c}.  Every element in the domain @{text H} of the supremum
+  function is member of the domain @{text H'} of some function @{text
+  h'}, such that @{text h} extends @{text h'}.
 *}
 
-lemma some_H'h': 
-  "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
-  graph H h = \<Union>c; x \<in> H |] 
-  ==> \<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 
+lemma some_H'h':
+  "M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
+  graph H h = \<Union>c \<Longrightarrow> x \<in> H
+  \<Longrightarrow> \<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
       \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
-      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x <= p x)" 
+      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
 proof -
   assume "M = norm_pres_extensions E p F f" and cM: "c \<in> chain M"
-     and u: "graph H h = \<Union>c" "x \<in> H"  
+     and u: "graph H h = \<Union>c"  "x \<in> H"
 
-  have "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h' 
-       \<and> is_linearform H' h' \<and> is_subspace H' E 
-       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
-       \<and> (\<forall>x \<in> H'. h' x <= p x)"
+  have "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
+       \<and> is_linearform H' h' \<and> is_subspace H' E
+       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+       \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
     by (rule some_H'h't)
-  thus ?thesis 
+  thus ?thesis
   proof (elim exE conjE)
-    fix H' h' assume "(x, h x) \<in> graph H' h'" "graph H' h' \<in> c"
-      "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" 
-      "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x <= p x"
+    fix H' h' assume "(x, h x) \<in> graph H' h'"  "graph H' h' \<in> c"
+      "is_linearform H' h'"  "is_subspace H' E"  "is_subspace F H'"
+      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
     show ?thesis
     proof (intro exI conjI)
       show "x \<in> H'" by (rule graphD1)
-      from cM u show "graph H' h' \<subseteq> graph H h" 
+      from cM u show "graph H' h' \<subseteq> graph H h"
         by (simp! only: chain_ball_Union_upper)
     qed
   qed
 qed
 
 
-text{* \medskip Any two elements $x$ and $y$ in the domain $H$ of the 
-supremum function $h$ are both in the domain $H'$ of some function 
-$h'$, such that $h$ extends $h'$. *}
+text {*
+  \medskip Any two elements @{text x} and @{text y} in the domain
+  @{text H} of the supremum function @{text h} are both in the domain
+  @{text H'} of some function @{text h'}, such that @{text h} extends
+  @{text h'}.
+*}
 
-lemma some_H'h'2: 
-  "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
-  graph H h = \<Union>c;  x \<in> H; y \<in> H |] 
-  ==> \<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h 
+lemma some_H'h'2:
+  "M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
+  graph H h = \<Union>c \<Longrightarrow> x \<in> H \<Longrightarrow> y \<in> H
+  \<Longrightarrow> \<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
       \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
-      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x <= p x)" 
+      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
 proof -
-  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" 
-         "graph H h = \<Union>c" "x \<in> H" "y \<in> H"
+  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"
+         "graph H h = \<Union>c"  "x \<in> H"  "y \<in> H"
 
-  txt {* $x$ is in the domain $H'$ of some function $h'$, 
-  such that $h$ extends $h'$. *} 
+  txt {*
+    @{text x} is in the domain @{text H'} of some function @{text h'},
+    such that @{text h} extends @{text h'}. *}
 
   have e1: "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h'
-       \<and> is_linearform H' h' \<and> is_subspace H' E 
-       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
-       \<and> (\<forall>x \<in> H'. h' x <= p x)"
+       \<and> is_linearform H' h' \<and> is_subspace H' E
+       \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+       \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
     by (rule some_H'h't)
 
-  txt {* $y$ is in the domain $H''$ of some function $h''$,
-  such that $h$ extends $h''$. *} 
+  txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
+  such that @{text h} extends @{text h''}. *}
 
   have e2: "\<exists>H'' h''. graph H'' h'' \<in> c \<and> (y, h y) \<in> graph H'' h''
-       \<and> is_linearform H'' h'' \<and> is_subspace H'' E 
-       \<and> is_subspace F H'' \<and> graph F f \<subseteq> graph H'' h'' 
-       \<and> (\<forall>x \<in> H''. h'' x <= p x)"
+       \<and> is_linearform H'' h'' \<and> is_subspace H'' E
+       \<and> is_subspace F H'' \<and> graph F f \<subseteq> graph H'' h''
+       \<and> (\<forall>x \<in> H''. h'' x \<le> p x)"
     by (rule some_H'h't)
 
-  from e1 e2 show ?thesis 
+  from e1 e2 show ?thesis
   proof (elim exE conjE)
-    fix H' h' assume "(y, h y) \<in> graph H' h'" "graph H' h' \<in> c"
-      "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" 
-      "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x <= p x"
+    fix H' h' assume "(y, h y) \<in> graph H' h'"  "graph H' h' \<in> c"
+      "is_linearform H' h'"  "is_subspace H' E"  "is_subspace F H'"
+      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
 
-    fix H'' h'' assume "(x, h x) \<in> graph H'' h''" "graph H'' h'' \<in> c"
-      "is_linearform H'' h''" "is_subspace H'' E" "is_subspace F H''"
-      "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x <= p x"
+    fix H'' h'' assume "(x, h x) \<in> graph H'' h''"  "graph H'' h'' \<in> c"
+      "is_linearform H'' h''"  "is_subspace H'' E"  "is_subspace F H''"
+      "graph F f \<subseteq> graph H'' h''"  "\<forall>x \<in> H''. h'' x \<le> p x"
 
-   txt {* Since both $h'$ and $h''$ are elements of the chain,  
-   $h''$ is an extension of $h'$ or vice versa. Thus both 
-   $x$ and $y$ are contained in the greater one. \label{cases1}*}
+   txt {* Since both @{text h'} and @{text h''} are elements of the chain,
+   @{text h''} is an extension of @{text h'} or vice versa. Thus both
+   @{text x} and @{text y} are contained in the greater one. \label{cases1}*}
 
-    have "graph H'' h'' \<subseteq> graph H' h' | graph H' h' \<subseteq> graph H'' h''"
-      (is "?case1 | ?case2")
+    have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
+      (is "?case1 \<or> ?case2")
       by (rule chainD)
     thus ?thesis
-    proof 
+    proof
       assume ?case1
       show ?thesis
       proof (intro exI conjI)
@@ -183,44 +191,47 @@
 
 
 
-text{* \medskip The relation induced by the graph of the supremum
-of a chain $c$ is definite, i.~e.~t is the graph of a function. *}
+text {*
+  \medskip The relation induced by the graph of the supremum of a
+  chain @{text c} is definite, i.~e.~t is the graph of a function. *}
 
-lemma sup_definite: 
-  "[| M == norm_pres_extensions E p F f; c \<in> chain M; 
-  (x, y) \<in> \<Union>c; (x, z) \<in> \<Union>c |] ==> z = y"
-proof - 
-  assume "c \<in> chain M" "M == norm_pres_extensions E p F f"
-    "(x, y) \<in> \<Union>c" "(x, z) \<in> \<Union>c"
+lemma sup_definite:
+  "M \<equiv> norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
+  (x, y) \<in> \<Union>c \<Longrightarrow> (x, z) \<in> \<Union>c \<Longrightarrow> z = y"
+proof -
+  assume "c \<in> chain M"  "M \<equiv> norm_pres_extensions E p F f"
+    "(x, y) \<in> \<Union>c"  "(x, z) \<in> \<Union>c"
   thus ?thesis
   proof (elim UnionE chainE2)
 
-    txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$
-    they are members of some graphs $G_1$ and $G_2$, resp., such that
-    both $G_1$ and $G_2$ are members of $c$.*}
+    txt {* Since both @{text "(x, y) \<in> \<Union>c"} and @{text "(x, z) \<in> \<Union>c"}
+    they are members of some graphs @{text "G\<^sub>1"} and @{text
+    "G\<^sub>2"}, resp., such that both @{text "G\<^sub>1"} and @{text
+    "G\<^sub>2"} are members of @{text c}.*}
 
     fix G1 G2 assume
-      "(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \<subseteq> M"
+      "(x, y) \<in> G1"  "G1 \<in> c"  "(x, z) \<in> G2"  "G2 \<in> c"  "c \<subseteq> M"
 
     have "G1 \<in> M" ..
-    hence e1: "\<exists>H1 h1. graph H1 h1 = G1"  
-      by (force! dest: norm_pres_extension_D)
+    hence e1: "\<exists>H1 h1. graph H1 h1 = G1"
+      by (blast! dest: norm_pres_extension_D)
     have "G2 \<in> M" ..
-    hence e2: "\<exists>H2 h2. graph H2 h2 = G2"  
-      by (force! dest: norm_pres_extension_D)
-    from e1 e2 show ?thesis 
+    hence e2: "\<exists>H2 h2. graph H2 h2 = G2"
+      by (blast! dest: norm_pres_extension_D)
+    from e1 e2 show ?thesis
     proof (elim exE)
-      fix H1 h1 H2 h2 
-      assume "graph H1 h1 = G1" "graph H2 h2 = G2"
+      fix H1 h1 H2 h2
+      assume "graph H1 h1 = G1"  "graph H2 h2 = G2"
 
-      txt{* $G_1$ is contained in $G_2$ or vice versa, 
-      since both $G_1$ and $G_2$ are members of $c$. \label{cases2}*}
+      txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
+      or vice versa, since both @{text "G\<^sub>1"} and @{text
+      "G\<^sub>2"} are members of @{text c}. \label{cases2}*}
 
-      have "G1 \<subseteq> G2 | G2 \<subseteq> G1" (is "?case1 | ?case2") ..
+      have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
       thus ?thesis
       proof
         assume ?case1
-        have "(x, y) \<in> graph H2 h2" by (force!)
+        have "(x, y) \<in> graph H2 h2" by (blast!)
         hence "y = h2 x" ..
         also have "(x, z) \<in> graph H2 h2" by (simp!)
         hence "z = h2 x" ..
@@ -229,7 +240,7 @@
         assume ?case2
         have "(x, y) \<in> graph H1 h1" by (simp!)
         hence "y = h1 x" ..
-        also have "(x, z) \<in> graph H1 h1" by (force!)
+        also have "(x, z) \<in> graph H1 h1" by (blast!)
         hence "z = h1 x" ..
         finally show ?thesis .
       qed
@@ -237,36 +248,39 @@
   qed
 qed
 
-text{* \medskip The limit function $h$ is linear. Every element $x$ in the
-domain of $h$ is in the domain of a function $h'$ in the chain of norm
-preserving extensions.  Furthermore, $h$ is an extension of $h'$ so
-the function values of $x$ are identical for $h'$ and $h$.  Finally, the
-function $h'$ is linear by construction of $M$.  *}
+text {*
+  \medskip The limit function @{text h} is linear. Every element
+  @{text x} in the domain of @{text h} is in the domain of a function
+  @{text h'} in the chain of norm preserving extensions.  Furthermore,
+  @{text h} is an extension of @{text h'} so the function values of
+  @{text x} are identical for @{text h'} and @{text h}.  Finally, the
+  function @{text h'} is linear by construction of @{text M}.
+*}
 
-lemma sup_lf: 
-  "[| M = norm_pres_extensions E p F f; c \<in> chain M; 
-  graph H h = \<Union>c |] ==> is_linearform H h"
-proof - 
-  assume "M = norm_pres_extensions E p F f" "c \<in> chain M"
+lemma sup_lf:
+  "M = norm_pres_extensions E p F f \<Longrightarrow> c \<in> chain M \<Longrightarrow>
+  graph H h = \<Union>c \<Longrightarrow> is_linearform H h"
+proof -
+  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"
          "graph H h = \<Union>c"
- 
+
   show "is_linearform H h"
   proof
-    fix x y assume "x \<in> H" "y \<in> H" 
-    have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h 
-            \<and> is_linearform H' h' \<and> is_subspace H' E 
+    fix x y assume "x \<in> H"  "y \<in> H"
+    have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
+            \<and> is_linearform H' h' \<and> is_subspace H' E
             \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
-            \<and> (\<forall>x \<in> H'. h' x <= p x)"
+            \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
       by (rule some_H'h'2)
 
-    txt {* We have to show that $h$ is additive. *}
+    txt {* We have to show that @{text h} is additive. *}
 
-    thus "h (x + y) = h x + h y" 
+    thus "h (x + y) = h x + h y"
     proof (elim exE conjE)
-      fix H' h' assume "x \<in> H'" "y \<in> H'" 
-        and b: "graph H' h' \<subseteq> graph H h" 
-        and "is_linearform H' h'" "is_subspace H' E"
-      have "h' (x + y) = h' x + h' y" 
+      fix H' h' assume "x \<in> H'"  "y \<in> H'"
+        and b: "graph H' h' \<subseteq> graph H h"
+        and "is_linearform H' h'"  "is_subspace H' E"
+      have "h' (x + y) = h' x + h' y"
         by (rule linearform_add)
       also have "h' x = h x" ..
       also have "h' y = h y" ..
@@ -274,22 +288,22 @@
       with b have "h' (x + y) = h (x + y)" ..
       finally show ?thesis .
     qed
-  next  
+  next
     fix a x assume "x \<in> H"
-    have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 
+    have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
             \<and> is_linearform H' h' \<and> is_subspace H' E
-            \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
-            \<and> (\<forall>x \<in> H'. h' x <= p x)"
+            \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+            \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
       by (rule some_H'h')
 
-    txt{* We have to show that $h$ is multiplicative. *}
+    txt{* We have to show that @{text h} is multiplicative. *}
 
     thus "h (a \<cdot> x) = a * h x"
     proof (elim exE conjE)
       fix H' h' assume "x \<in> H'"
-        and b: "graph H' h' \<subseteq> graph H h" 
-        and "is_linearform H' h'" "is_subspace H' E"
-      have "h' (a \<cdot> x) = a * h' x" 
+        and b: "graph H' h' \<subseteq> graph H h"
+        and "is_linearform H' h'"  "is_subspace H' E"
+      have "h' (a \<cdot> x) = a * h' x"
         by (rule linearform_mult)
       also have "h' x = h x" ..
       also have "a \<cdot> x \<in> H'" ..
@@ -299,36 +313,37 @@
   qed
 qed
 
-text{* \medskip The limit of a non-empty chain of norm
-preserving extensions of $f$ is an extension of $f$,
-since every element of the chain is an extension
-of $f$ and the supremum is an extension
-for every element of the chain.*}
+text {*
+  \medskip The limit of a non-empty chain of norm preserving
+  extensions of @{text f} is an extension of @{text f}, since every
+  element of the chain is an extension of @{text f} and the supremum
+  is an extension for every element of the chain.
+*}
 
 lemma sup_ext:
-  "[| graph H h = \<Union>c; M = norm_pres_extensions E p F f; 
-  c \<in> chain M; \<exists>x. x \<in> c |] ==> graph F f \<subseteq> graph H h"
+  "graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
+  c \<in> chain M \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> graph F f \<subseteq> graph H h"
 proof -
-  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" 
+  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"
          "graph H h = \<Union>c"
   assume "\<exists>x. x \<in> c"
-  thus ?thesis 
+  thus ?thesis
   proof
-    fix x assume "x \<in> c" 
+    fix x assume "x \<in> c"
     have "c \<subseteq> M" by (rule chainD2)
     hence "x \<in> M" ..
     hence "x \<in> norm_pres_extensions E p F f" by (simp!)
 
     hence "\<exists>G g. graph G g = x
-             \<and> is_linearform G g 
+             \<and> is_linearform G g
              \<and> is_subspace G E
              \<and> is_subspace F G
-             \<and> graph F f \<subseteq> graph G g 
-             \<and> (\<forall>x \<in> G. g x <= p x)"
+             \<and> graph F f \<subseteq> graph G g
+             \<and> (\<forall>x \<in> G. g x \<le> p x)"
       by (simp! add: norm_pres_extension_D)
 
-    thus ?thesis 
-    proof (elim exE conjE) 
+    thus ?thesis
+    proof (elim exE conjE)
       fix G g assume "graph F f \<subseteq> graph G g"
       also assume "graph G g = x"
       also have "... \<in> c" .
@@ -339,30 +354,32 @@
   qed
 qed
 
-text{* \medskip The domain $H$ of the limit function is a superspace of $F$,
-since $F$ is a subset of $H$. The existence of the $\zero$ element in
-$F$ and the closure properties follow from the fact that $F$ is a
-vector space. *}
+text {*
+  \medskip The domain @{text H} of the limit function is a superspace
+  of @{text F}, since @{text F} is a subset of @{text H}. The
+  existence of the @{text 0} element in @{text F} and the closure
+  properties follow from the fact that @{text F} is a vector space.
+*}
 
-lemma sup_supF: 
-  "[|  graph H h = \<Union>c; M = norm_pres_extensions E p F f; 
-  c \<in> chain M; \<exists>x. x \<in> c; is_subspace F E; is_vectorspace E |] 
-  ==> is_subspace F H"
-proof - 
-  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c"
-    "graph H h = \<Union>c" "is_subspace F E" "is_vectorspace E"
+lemma sup_supF:
+  "graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
+  c \<in> chain M \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> is_subspace F E \<Longrightarrow> is_vectorspace E
+  \<Longrightarrow> is_subspace F H"
+proof -
+  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"  "\<exists>x. x \<in> c"
+    "graph H h = \<Union>c"  "is_subspace F E"  "is_vectorspace E"
 
-  show ?thesis 
+  show ?thesis
   proof
     show "0 \<in> F" ..
-    show "F \<subseteq> H" 
+    show "F \<subseteq> H"
     proof (rule graph_extD2)
       show "graph F f \<subseteq> graph H h"
         by (rule sup_ext)
     qed
-    show "\<forall>x \<in> F. \<forall>y \<in> F. x + y \<in> F" 
-    proof (intro ballI) 
-      fix x y assume "x \<in> F" "y \<in> F"
+    show "\<forall>x \<in> F. \<forall>y \<in> F. x + y \<in> F"
+    proof (intro ballI)
+      fix x y assume "x \<in> F"  "y \<in> F"
       show "x + y \<in> F" by (simp!)
     qed
     show "\<forall>x \<in> F. \<forall>a. a \<cdot> x \<in> F"
@@ -373,166 +390,171 @@
   qed
 qed
 
-text{* \medskip The domain $H$ of the limit function is a subspace
-of $E$. *}
+text {*
+  \medskip The domain @{text H} of the limit function is a subspace of
+  @{text E}.
+*}
 
-lemma sup_subE: 
-  "[| graph H h = \<Union>c; M = norm_pres_extensions E p F f; 
-  c \<in> chain M; \<exists>x. x \<in> c; is_subspace F E; is_vectorspace E |] 
-  ==> is_subspace H E"
-proof - 
-  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c"
-    "graph H h = \<Union>c" "is_subspace F E" "is_vectorspace E"
-  show ?thesis 
+lemma sup_subE:
+  "graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
+  c \<in> chain M \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> is_subspace F E \<Longrightarrow> is_vectorspace E
+  \<Longrightarrow> is_subspace H E"
+proof -
+  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"  "\<exists>x. x \<in> c"
+    "graph H h = \<Union>c"  "is_subspace F E"  "is_vectorspace E"
+  show ?thesis
   proof
- 
-    txt {* The $\zero$ element is in $H$, as $F$ is a subset 
-    of $H$: *}
+
+    txt {* The @{text 0} element is in @{text H}, as @{text F} is a
+    subset of @{text H}: *}
 
     have "0 \<in> F" ..
-    also have "is_subspace F H" by (rule sup_supF) 
+    also have "is_subspace F H" by (rule sup_supF)
     hence "F \<subseteq> H" ..
     finally show "0 \<in> H" .
 
-    txt{* $H$ is a subset of $E$: *}
+    txt {* @{text H} is a subset of @{text E}: *}
 
-    show "H \<subseteq> E" 
+    show "H \<subseteq> E"
     proof
       fix x assume "x \<in> H"
       have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
-              \<and> is_linearform H' h' \<and> is_subspace H' E 
-              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
-              \<and> (\<forall>x \<in> H'. h' x <= p x)" 
-	by (rule some_H'h')
-      thus "x \<in> E" 
+              \<and> is_linearform H' h' \<and> is_subspace H' E
+              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+              \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
+        by (rule some_H'h')
+      thus "x \<in> E"
       proof (elim exE conjE)
-	fix H' h' assume "x \<in> H'" "is_subspace H' E"
+        fix H' h' assume "x \<in> H'"  "is_subspace H' E"
         have "H' \<subseteq> E" ..
-	thus "x \<in> E" ..
+        thus "x \<in> E" ..
       qed
     qed
 
-    txt{* $H$ is closed under addition: *}
+    txt {* @{text H} is closed under addition: *}
 
-    show "\<forall>x \<in> H. \<forall>y \<in> H. x + y \<in> H" 
-    proof (intro ballI) 
-      fix x y assume "x \<in> H" "y \<in> H"
-      have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h 
-              \<and> is_linearform H' h' \<and> is_subspace H' E 
-              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
-              \<and> (\<forall>x \<in> H'. h' x <= p x)" 
-	by (rule some_H'h'2) 
-      thus "x + y \<in> H" 
-      proof (elim exE conjE) 
-	fix H' h' 
-        assume "x \<in> H'" "y \<in> H'" "is_subspace H' E" 
+    show "\<forall>x \<in> H. \<forall>y \<in> H. x + y \<in> H"
+    proof (intro ballI)
+      fix x y assume "x \<in> H"  "y \<in> H"
+      have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h
+              \<and> is_linearform H' h' \<and> is_subspace H' E
+              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+              \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
+        by (rule some_H'h'2)
+      thus "x + y \<in> H"
+      proof (elim exE conjE)
+        fix H' h'
+        assume "x \<in> H'"  "y \<in> H'"  "is_subspace H' E"
           "graph H' h' \<subseteq> graph H h"
         have "x + y \<in> H'" ..
-	also have "H' \<subseteq> H" ..
-	finally show ?thesis .
+        also have "H' \<subseteq> H" ..
+        finally show ?thesis .
       qed
-    qed      
+    qed
 
-    txt{* $H$ is closed under scalar multiplication: *}
+    txt {* @{text H} is closed under scalar multiplication: *}
 
-    show "\<forall>x \<in> H. \<forall>a. a \<cdot> x \<in> H" 
-    proof (intro ballI allI) 
-      fix x a assume "x \<in> H" 
+    show "\<forall>x \<in> H. \<forall>a. a \<cdot> x \<in> H"
+    proof (intro ballI allI)
+      fix x a assume "x \<in> H"
       have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
-              \<and> is_linearform H' h' \<and> is_subspace H' E 
-              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' 
-              \<and> (\<forall>x \<in> H'. h' x <= p x)" 
-	by (rule some_H'h') 
-      thus "a \<cdot> x \<in> H" 
+              \<and> is_linearform H' h' \<and> is_subspace H' E
+              \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h'
+              \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
+        by (rule some_H'h')
+      thus "a \<cdot> x \<in> H"
       proof (elim exE conjE)
-	fix H' h' 
-        assume "x \<in> H'" "is_subspace H' E" "graph H' h' \<subseteq> graph H h"
+        fix H' h'
+        assume "x \<in> H'"  "is_subspace H' E"  "graph H' h' \<subseteq> graph H h"
         have "a \<cdot> x \<in> H'" ..
         also have "H' \<subseteq> H" ..
-	finally show ?thesis .
+        finally show ?thesis .
       qed
     qed
   qed
 qed
 
-text {* \medskip The limit function is bounded by 
-the norm $p$ as well, since all elements in the chain are
-bounded by $p$.
+text {*
+  \medskip The limit function is bounded by the norm @{text p} as
+  well, since all elements in the chain are bounded by @{text p}.
 *}
 
 lemma sup_norm_pres:
-  "[| graph H h = \<Union>c; M = norm_pres_extensions E p F f; 
-  c \<in> chain M |] ==> \<forall>x \<in> H. h x <= p x"
+  "graph H h = \<Union>c \<Longrightarrow> M = norm_pres_extensions E p F f \<Longrightarrow>
+  c \<in> chain M \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x"
 proof
-  assume "M = norm_pres_extensions E p F f" "c \<in> chain M" 
+  assume "M = norm_pres_extensions E p F f"  "c \<in> chain M"
          "graph H h = \<Union>c"
   fix x assume "x \<in> H"
-  have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 
+  have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
           \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H'
-          \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x <= p x)" 
+          \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
     by (rule some_H'h')
-  thus "h x <= p x" 
+  thus "h x \<le> p x"
   proof (elim exE conjE)
-    fix H' h' 
-    assume "x \<in> H'" "graph H' h' \<subseteq> graph H h" 
-      and a: "\<forall>x \<in> H'. h' x <= p x"
+    fix H' h'
+    assume "x \<in> H'"  "graph H' h' \<subseteq> graph H h"
+      and a: "\<forall>x \<in> H'. h' x \<le> p x"
     have [symmetric]: "h' x = h x" ..
-    also from a have "h' x <= p x " ..
-    finally show ?thesis .  
+    also from a have "h' x \<le> p x " ..
+    finally show ?thesis .
   qed
 qed
 
 
-text{* \medskip The following lemma is a property of linear forms on 
-real vector spaces. It will be used for the lemma 
-$\idt{abs{\dsh}HahnBanach}$ (see page \pageref{abs-HahnBanach}). \label{abs-ineq-iff}
-For real vector spaces the following inequations are equivalent:
-\begin{matharray}{ll} 
-\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\ 
-\forall x\in H.\ap h\ap x\leq p\ap x\\ 
-\end{matharray}
+text {*
+  \medskip The following lemma is a property of linear forms on real
+  vector spaces. It will be used for the lemma @{text abs_HahnBanach}
+  (see page \pageref{abs-HahnBanach}). \label{abs-ineq-iff} For real
+  vector spaces the following inequations are equivalent:
+  \begin{center}
+  \begin{tabular}{lll}
+  @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
+  @{text "\<forall>x \<in> H. h x \<le> p x"} \\
+  \end{tabular}
+  \end{center}
 *}
 
-lemma abs_ineq_iff: 
-  "[| is_subspace H E; is_vectorspace E; is_seminorm E p; 
-  is_linearform H h |] 
-  ==> (\<forall>x \<in> H. |h x| <= p x) = (\<forall>x \<in> H. h x <= p x)" 
+lemma abs_ineq_iff:
+  "is_subspace H E \<Longrightarrow> is_vectorspace E \<Longrightarrow> is_seminorm E p \<Longrightarrow>
+  is_linearform H h
+  \<Longrightarrow> (\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)"
   (concl is "?L = ?R")
 proof -
-  assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p" 
+  assume "is_subspace H E"  "is_vectorspace E"  "is_seminorm E p"
          "is_linearform H h"
   have h: "is_vectorspace H" ..
   show ?thesis
-  proof 
+  proof
     assume l: ?L
     show ?R
     proof
       fix x assume x: "x \<in> H"
-      have "h x <= |h x|" by (rule abs_ge_self)
-      also from l have "... <= p x" ..
-      finally show "h x <= p x" .
+      have "h x \<le> \<bar>h x\<bar>" by (rule abs_ge_self)
+      also from l have "... \<le> p x" ..
+      finally show "h x \<le> p x" .
     qed
   next
     assume r: ?R
     show ?L
-    proof 
+    proof
       fix x assume "x \<in> H"
-      show "!! a b :: real. [| - a <= b; b <= a |] ==> |b| <= a"
+      show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
         by arith
-      show "- p x <= h x"
+      show "- p x \<le> h x"
       proof (rule real_minus_le)
-	from h have "- h x = h (- x)"
+        from h have "- h x = h (- x)"
           by (rule linearform_neg [symmetric])
-	also from r have "... <= p (- x)" by (simp!)
-	also have "... = p x" 
+        also from r have "... \<le> p (- x)" by (simp!)
+        also have "... = p x"
         proof (rule seminorm_minus)
           show "x \<in> E" ..
         qed
-	finally show "- h x <= p x" . 
+        finally show "- h x \<le> p x" .
       qed
-      from r show "h x <= p x" .. 
+      from r show "h x \<le> p x" ..
     qed
   qed
-qed  
+qed
 
-end
\ No newline at end of file
+end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -7,63 +7,65 @@
 
 theory Linearform = VectorSpace:
 
-text{* A \emph{linear form} is a function on a vector
-space into the reals that is additive and multiplicative. *}
+text {*
+  A \emph{linear form} is a function on a vector space into the reals
+  that is additive and multiplicative.
+*}
 
 constdefs
-  is_linearform :: "['a::{plus, minus, zero} set, 'a => real] => bool" 
-  "is_linearform V f == 
+  is_linearform :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
+  "is_linearform V f \<equiv>
       (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>
-      (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))" 
+      (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))"
 
-lemma is_linearformI [intro]: 
-  "[| !! x y. [| x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y;
-    !! x c. x \<in> V ==> f (c \<cdot> x) = c * f x |]
- ==> is_linearform V f"
- by (unfold is_linearform_def) force
+lemma is_linearformI [intro]:
+  "(\<And>x y. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y) \<Longrightarrow>
+    (\<And>x c. x \<in> V \<Longrightarrow> f (c \<cdot> x) = c * f x)
+ \<Longrightarrow> is_linearform V f"
+ by (unfold is_linearform_def) blast
 
-lemma linearform_add [intro?]: 
-  "[| is_linearform V f; x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y"
-  by (unfold is_linearform_def) fast
+lemma linearform_add [intro?]:
+  "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
+  by (unfold is_linearform_def) blast
 
-lemma linearform_mult [intro?]: 
-  "[| is_linearform V f; x \<in> V |] ==>  f (a \<cdot> x) = a * (f x)" 
-  by (unfold is_linearform_def) fast
+lemma linearform_mult [intro?]:
+  "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow>  f (a \<cdot> x) = a * (f x)"
+  by (unfold is_linearform_def) blast
 
 lemma linearform_neg [intro?]:
-  "[|  is_vectorspace V; is_linearform V f; x \<in> V|] 
-  ==> f (- x) = - f x"
-proof - 
-  assume "is_linearform V f" "is_vectorspace V" "x \<in> V"
+  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V
+  \<Longrightarrow> f (- x) = - f x"
+proof -
+  assume "is_linearform V f"  "is_vectorspace V"  "x \<in> V"
   have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1)
   also have "... = (- #1) * (f x)" by (rule linearform_mult)
   also have "... = - (f x)" by (simp!)
   finally show ?thesis .
 qed
 
-lemma linearform_diff [intro?]: 
-  "[| is_vectorspace V; is_linearform V f; x \<in> V; y \<in> V |] 
-  ==> f (x - y) = f x - f y"  
+lemma linearform_diff [intro?]:
+  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
+  \<Longrightarrow> f (x - y) = f x - f y"
 proof -
-  assume "is_vectorspace V" "is_linearform V f" "x \<in> V" "y \<in> V"
+  assume "is_vectorspace V"  "is_linearform V f"  "x \<in> V"  "y \<in> V"
   have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)
-  also have "... = f x + f (- y)" 
+  also have "... = f x + f (- y)"
     by (rule linearform_add) (simp!)+
   also have "f (- y) = - f y" by (rule linearform_neg)
   finally show "f (x - y) = f x - f y" by (simp!)
 qed
 
-text{* Every linear form yields $0$ for the $\zero$ vector.*}
+text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
 
-lemma linearform_zero [intro?, simp]: 
-  "[| is_vectorspace V; is_linearform V f |] ==> f 0 = #0"
-proof - 
-  assume "is_vectorspace V" "is_linearform V f"
+lemma linearform_zero [intro?, simp]:
+  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> f 0 = #0"
+proof -
+  assume "is_vectorspace V"  "is_linearform V f"
   have "f 0 = f (0 - 0)" by (simp!)
-  also have "... = f 0 - f 0" 
+  also have "... = f 0 - f 0"
     by (rule linearform_diff) (simp!)+
   also have "... = #0" by simp
   finally show "f 0 = #0" .
-qed 
+qed
 
-end
\ No newline at end of file
+end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -7,96 +7,97 @@
 
 theory NormedSpace =  Subspace:
 
-syntax 
-  abs :: "real \<Rightarrow> real" ("|_|")
-
 subsection {* Quasinorms *}
 
-text{* A \emph{seminorm} $\norm{\cdot}$ is a function on a real vector
-space into the reals that has the following properties: It is positive
-definite, absolute homogenous and subadditive.  *}
+text {*
+  A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
+  into the reals that has the following properties: it is positive
+  definite, absolute homogenous and subadditive.
+*}
 
 constdefs
-  is_seminorm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
-  "is_seminorm V norm == \<forall>x \<in>  V. \<forall>y \<in> V. \<forall>a. 
-        #0 <= norm x 
-      \<and> norm (a \<cdot> x) = |a| * norm x
-      \<and> norm (x + y) <= norm x + norm y"
+  is_seminorm :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
+  "is_seminorm V norm \<equiv> \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a.
+        #0 \<le> norm x
+      \<and> norm (a \<cdot> x) = \<bar>a\<bar> * norm x
+      \<and> norm (x + y) \<le> norm x + norm y"
 
-lemma is_seminormI [intro]: 
-  "[| !! x y a. [| x \<in> V; y \<in> V|] ==> #0 <= norm x;
-  !! x a. x \<in> V ==> norm (a \<cdot> x) = |a| * norm x;
-  !! x y. [|x \<in> V; y \<in> V |] ==> norm (x + y) <= norm x + norm y |] 
-  ==> is_seminorm V norm"
-  by (unfold is_seminorm_def, force)
+lemma is_seminormI [intro]:
+  "(\<And>x y a. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> #0 \<le> norm x) \<Longrightarrow>
+  (\<And>x a. x \<in> V \<Longrightarrow> norm (a \<cdot> x) = \<bar>a\<bar> * norm x) \<Longrightarrow>
+  (\<And>x y. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> norm (x + y) \<le> norm x + norm y)
+  \<Longrightarrow> is_seminorm V norm"
+  by (unfold is_seminorm_def) auto
 
 lemma seminorm_ge_zero [intro?]:
-  "[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x"
-  by (unfold is_seminorm_def, force)
+  "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> #0 \<le> norm x"
+  by (unfold is_seminorm_def) blast
 
-lemma seminorm_abs_homogenous: 
-  "[| is_seminorm V norm; x \<in> V |] 
-  ==> norm (a \<cdot> x) = |a| * norm x"
-  by (unfold is_seminorm_def, force)
+lemma seminorm_abs_homogenous:
+  "is_seminorm V norm \<Longrightarrow> x \<in> V
+  \<Longrightarrow> norm (a \<cdot> x) = \<bar>a\<bar> * norm x"
+  by (unfold is_seminorm_def) blast
 
-lemma seminorm_subadditive: 
-  "[| is_seminorm V norm; x \<in> V; y \<in> V |] 
-  ==> norm (x + y) <= norm x + norm y"
-  by (unfold is_seminorm_def, force)
+lemma seminorm_subadditive:
+  "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
+  \<Longrightarrow> norm (x + y) \<le> norm x + norm y"
+  by (unfold is_seminorm_def) blast
 
-lemma seminorm_diff_subadditive: 
-  "[| is_seminorm V norm; x \<in> V; y \<in> V; is_vectorspace V |] 
-  ==> norm (x - y) <= norm x + norm y"
+lemma seminorm_diff_subadditive:
+  "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> is_vectorspace V
+  \<Longrightarrow> norm (x - y) \<le> norm x + norm y"
 proof -
-  assume "is_seminorm V norm" "x \<in> V" "y \<in> V" "is_vectorspace V"
-  have "norm (x - y) = norm (x + - #1 \<cdot> y)"  
+  assume "is_seminorm V norm"  "x \<in> V"  "y \<in> V"  "is_vectorspace V"
+  have "norm (x - y) = norm (x + - #1 \<cdot> y)"
     by (simp! add: diff_eq2 negate_eq2a)
-  also have "... <= norm x + norm  (- #1 \<cdot> y)" 
+  also have "... \<le> norm x + norm  (- #1 \<cdot> y)"
     by (simp! add: seminorm_subadditive)
-  also have "norm (- #1 \<cdot> y) = |- #1| * norm y" 
+  also have "norm (- #1 \<cdot> y) = \<bar>- #1\<bar> * norm y"
     by (rule seminorm_abs_homogenous)
-  also have "|- #1| = (#1::real)" by (rule abs_minus_one)
-  finally show "norm (x - y) <= norm x + norm y" by simp
+  also have "\<bar>- #1\<bar> = (#1::real)" by (rule abs_minus_one)
+  finally show "norm (x - y) \<le> norm x + norm y" by simp
 qed
 
-lemma seminorm_minus: 
-  "[| is_seminorm V norm; x \<in> V; is_vectorspace V |] 
-  ==> norm (- x) = norm x"
+lemma seminorm_minus:
+  "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> is_vectorspace V
+  \<Longrightarrow> norm (- x) = norm x"
 proof -
-  assume "is_seminorm V norm" "x \<in> V" "is_vectorspace V"
+  assume "is_seminorm V norm"  "x \<in> V"  "is_vectorspace V"
   have "norm (- x) = norm (- #1 \<cdot> x)" by (simp! only: negate_eq1)
-  also have "... = |- #1| * norm x" 
+  also have "... = \<bar>- #1\<bar> * norm x"
     by (rule seminorm_abs_homogenous)
-  also have "|- #1| = (#1::real)" by (rule abs_minus_one)
+  also have "\<bar>- #1\<bar> = (#1::real)" by (rule abs_minus_one)
   finally show "norm (- x) = norm x" by simp
 qed
 
 
 subsection {* Norms *}
 
-text{* A \emph{norm} $\norm{\cdot}$ is a seminorm that maps only the
-$\zero$ vector to $0$. *}
+text {*
+  A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
+  @{text 0} vector to @{text 0}.
+*}
 
 constdefs
-  is_norm :: "['a::{plus, minus, zero} set, 'a => real] => bool"
-  "is_norm V norm == \<forall>x \<in> V.  is_seminorm V norm 
+  is_norm :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
+  "is_norm V norm \<equiv> \<forall>x \<in> V. is_seminorm V norm
       \<and> (norm x = #0) = (x = 0)"
 
-lemma is_normI [intro]: 
-  "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = #0) = (x = 0) 
-  ==> is_norm V norm" by (simp only: is_norm_def)
+lemma is_normI [intro]:
+  "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = #0) = (x = 0)
+  \<Longrightarrow> is_norm V norm" by (simp only: is_norm_def)
 
-lemma norm_is_seminorm [intro?]: 
-  "[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm"
-  by (unfold is_norm_def, force)
+lemma norm_is_seminorm [intro?]:
+  "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> is_seminorm V norm"
+  by (unfold is_norm_def) blast
 
-lemma norm_zero_iff: 
-  "[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)"
-  by (unfold is_norm_def, force)
+lemma norm_zero_iff:
+  "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> (norm x = #0) = (x = 0)"
+  by (unfold is_norm_def) blast
 
 lemma norm_ge_zero [intro?]:
-  "[|is_norm V norm; x \<in> V |] ==> #0 <= norm x"
-  by (unfold is_norm_def is_seminorm_def, force)
+  "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> #0 \<le> norm x"
+  by (unfold is_norm_def is_seminorm_def) blast
 
 
 subsection {* Normed vector spaces *}
@@ -105,33 +106,33 @@
 a \emph{normed space}. *}
 
 constdefs
-  is_normed_vectorspace :: 
-  "['a::{plus, minus, zero} set, 'a => real] => bool"
-  "is_normed_vectorspace V norm ==
+  is_normed_vectorspace ::
+  "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
+  "is_normed_vectorspace V norm \<equiv>
       is_vectorspace V \<and> is_norm V norm"
 
-lemma normed_vsI [intro]: 
-  "[| is_vectorspace V; is_norm V norm |] 
-  ==> is_normed_vectorspace V norm"
-  by (unfold is_normed_vectorspace_def) blast 
+lemma normed_vsI [intro]:
+  "is_vectorspace V \<Longrightarrow> is_norm V norm
+  \<Longrightarrow> 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"
-  by (unfold is_normed_vectorspace_def) force
+lemma normed_vs_vs [intro?]:
+  "is_normed_vectorspace V norm \<Longrightarrow> is_vectorspace V"
+  by (unfold is_normed_vectorspace_def) blast
 
-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 [intro?]:
+  "is_normed_vectorspace V norm \<Longrightarrow> is_norm V norm"
+  by (unfold is_normed_vectorspace_def) blast
 
-lemma normed_vs_norm_ge_zero [intro?]: 
-  "[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x"
-  by (unfold is_normed_vectorspace_def, rule, elim conjE)
+lemma normed_vs_norm_ge_zero [intro?]:
+  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V \<Longrightarrow> #0 \<le> norm x"
+  by (unfold is_normed_vectorspace_def) (fast elim: norm_ge_zero)
 
-lemma normed_vs_norm_gt_zero [intro?]: 
-  "[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x"
+lemma normed_vs_norm_gt_zero [intro?]:
+  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> #0 < norm x"
 proof (unfold is_normed_vectorspace_def, elim conjE)
-  assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm"
-  have "#0 <= norm x" ..
+  assume "x \<in> V"  "x \<noteq> 0"  "is_vectorspace V"  "is_norm V norm"
+  have "#0 \<le> norm x" ..
   also have "#0 \<noteq> norm x"
   proof
     presume "norm x = #0"
@@ -142,45 +143,45 @@
   finally show "#0 < norm x" .
 qed
 
-lemma normed_vs_norm_abs_homogenous [intro?]: 
-  "[| is_normed_vectorspace V norm; x \<in> V |] 
-  ==> norm (a \<cdot> x) = |a| * norm x"
-  by (rule seminorm_abs_homogenous, rule norm_is_seminorm, 
+lemma normed_vs_norm_abs_homogenous [intro?]:
+  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V
+  \<Longrightarrow> norm (a \<cdot> x) = \<bar>a\<bar> * norm x"
+  by (rule seminorm_abs_homogenous, rule norm_is_seminorm,
       rule normed_vs_norm)
 
-lemma normed_vs_norm_subadditive [intro?]: 
-  "[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |] 
-  ==> norm (x + y) <= norm x + norm y"
-  by (rule seminorm_subadditive, rule norm_is_seminorm, 
+lemma normed_vs_norm_subadditive [intro?]:
+  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
+  \<Longrightarrow> norm (x + y) \<le> norm x + norm y"
+  by (rule seminorm_subadditive, rule norm_is_seminorm,
      rule normed_vs_norm)
 
-text{* Any subspace of a normed vector space is again a 
+text{* Any subspace of a normed vector space is again a
 normed vectorspace.*}
 
-lemma subspace_normed_vs [intro?]: 
-  "[| is_vectorspace E; is_subspace F E;
-  is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"
+lemma subspace_normed_vs [intro?]:
+  "is_vectorspace E \<Longrightarrow> is_subspace F E \<Longrightarrow>
+  is_normed_vectorspace E norm \<Longrightarrow> is_normed_vectorspace F norm"
 proof (rule normed_vsI)
-  assume "is_subspace F E" "is_vectorspace E" 
+  assume "is_subspace F E"  "is_vectorspace E"
          "is_normed_vectorspace E norm"
   show "is_vectorspace F" ..
-  show "is_norm F norm" 
+  show "is_norm F norm"
   proof (intro is_normI ballI conjI)
-    show "is_seminorm F norm" 
+    show "is_seminorm F norm"
     proof
       fix x y a presume "x \<in> E"
-      show "#0 <= norm x" ..
-      show "norm (a \<cdot> x) = |a| * norm x" ..
+      show "#0 \<le> norm x" ..
+      show "norm (a \<cdot> x) = \<bar>a\<bar> * norm x" ..
       presume "y \<in> E"
-      show "norm (x + y) <= norm x + norm y" ..
+      show "norm (x + y) \<le> norm x + norm y" ..
     qed (simp!)+
 
     fix x assume "x \<in> F"
-    show "(norm x = #0) = (x = 0)" 
+    show "(norm x = #0) = (x = 0)"
     proof (rule norm_zero_iff)
       show "is_norm E norm" ..
     qed (simp!)
   qed
 qed
 
-end
\ No newline at end of file
+end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -3,7 +3,6 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-
 header {* Subspaces *}
 
 theory Subspace = VectorSpace:
@@ -11,59 +10,61 @@
 
 subsection {* Definition *}
 
-text {* A non-empty subset $U$ of a vector space $V$ is a 
-\emph{subspace} of $V$, iff $U$ is closed under addition and 
-scalar multiplication. *}
+text {*
+  A non-empty subset @{text U} of a vector space @{text V} is a
+  \emph{subspace} of @{text V}, iff @{text U} is closed under addition
+  and scalar multiplication.
+*}
 
-constdefs 
-  is_subspace ::  "['a::{plus, minus, zero} set, 'a set] => bool"
-  "is_subspace U V == U \<noteq> {} \<and> U <= V 
-     \<and> (\<forall>x \<in> U. \<forall>y \<in> U. \<forall>a. x + y \<in> U \<and> a \<cdot> x\<in> U)"
+constdefs
+  is_subspace ::  "'a::{plus, minus, zero} set \<Rightarrow> 'a set \<Rightarrow> bool"
+  "is_subspace U V \<equiv> U \<noteq> {} \<and> U \<subseteq> V
+     \<and> (\<forall>x \<in> U. \<forall>y \<in> U. \<forall>a. x + y \<in> U \<and> a \<cdot> x \<in> U)"
 
-lemma subspaceI [intro]: 
-  "[| 0 \<in> U; U <= V; \<forall>x \<in> U. \<forall>y \<in> U. (x + y \<in> U); 
-  \<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U |]
-  ==> is_subspace U V"
-proof (unfold is_subspace_def, intro conjI) 
+lemma subspaceI [intro]:
+  "0 \<in> U \<Longrightarrow> U \<subseteq> V \<Longrightarrow> \<forall>x \<in> U. \<forall>y \<in> U. (x + y \<in> U) \<Longrightarrow>
+  \<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U
+  \<Longrightarrow> is_subspace U V"
+proof (unfold is_subspace_def, intro conjI)
   assume "0 \<in> U" thus "U \<noteq> {}" by fast
 qed (simp+)
 
-lemma subspace_not_empty [intro?]: "is_subspace U V ==> U \<noteq> {}"
-  by (unfold is_subspace_def) simp 
+lemma subspace_not_empty [intro?]: "is_subspace U V \<Longrightarrow> U \<noteq> {}"
+  by (unfold is_subspace_def) blast
 
-lemma subspace_subset [intro?]: "is_subspace U V ==> U <= V"
-  by (unfold is_subspace_def) simp
+lemma subspace_subset [intro?]: "is_subspace U V \<Longrightarrow> U \<subseteq> V"
+  by (unfold is_subspace_def) blast
 
-lemma subspace_subsetD [simp, intro?]: 
-  "[| is_subspace U V; x \<in> U |] ==> x \<in> V"
-  by (unfold is_subspace_def) force
+lemma subspace_subsetD [simp, intro?]:
+  "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> x \<in> V"
+  by (unfold is_subspace_def) blast
 
-lemma subspace_add_closed [simp, intro?]: 
-  "[| is_subspace U V; x \<in> U; y \<in> U |] ==> x + y \<in> U"
-  by (unfold is_subspace_def) simp
+lemma subspace_add_closed [simp, intro?]:
+  "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
+  by (unfold is_subspace_def) blast
 
-lemma subspace_mult_closed [simp, intro?]: 
-  "[| is_subspace U V; x \<in> U |] ==> a \<cdot> x \<in> U"
-  by (unfold is_subspace_def) simp
+lemma subspace_mult_closed [simp, intro?]:
+  "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
+  by (unfold is_subspace_def) blast
 
-lemma subspace_diff_closed [simp, intro?]: 
-  "[| is_subspace U V; is_vectorspace V; x \<in> U; y \<in> U |] 
-  ==> x - y \<in> U"
-  by (simp! add: diff_eq1 negate_eq1)
+lemma subspace_diff_closed [simp, intro?]:
+  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> x \<in> U \<Longrightarrow> y \<in> U
+  \<Longrightarrow> x - y \<in> U"
+  by (simp add: diff_eq1 negate_eq1)
 
-text {* Similar as for linear spaces, the existence of the 
-zero element in every subspace follows from the non-emptiness 
+text {* Similar as for linear spaces, the existence of the
+zero element in every subspace follows from the non-emptiness
 of the carrier set and by vector space laws.*}
 
 lemma zero_in_subspace [intro?]:
-  "[| is_subspace U V; is_vectorspace V |] ==> 0 \<in> U"
-proof - 
+  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> 0 \<in> U"
+proof -
   assume "is_subspace U V" and v: "is_vectorspace V"
   have "U \<noteq> {}" ..
-  hence "\<exists>x. x \<in> U" by force
-  thus ?thesis 
-  proof 
-    fix x assume u: "x \<in> U" 
+  hence "\<exists>x. x \<in> U" by blast
+  thus ?thesis
+  proof
+    fix x assume u: "x \<in> U"
     hence "x \<in> V" by (simp!)
     with v have "0 = x - x" by (simp!)
     also have "... \<in> U" by (rule subspace_diff_closed)
@@ -71,55 +72,54 @@
   qed
 qed
 
-lemma subspace_neg_closed [simp, intro?]: 
-  "[| is_subspace U V; is_vectorspace V; x \<in> U |] ==> - x \<in> U"
+lemma subspace_neg_closed [simp, intro?]:
+  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> x \<in> U \<Longrightarrow> - x \<in> U"
   by (simp add: negate_eq1)
 
-text_raw {* \medskip *}
-text {* Further derived laws: every subspace is a vector space. *}
+text {* \medskip Further derived laws: every subspace is a vector space. *}
 
 lemma subspace_vs [intro?]:
-  "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U"
+  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> is_vectorspace U"
 proof -
-  assume "is_subspace U V" "is_vectorspace V"
+  assume "is_subspace U V"  "is_vectorspace V"
   show ?thesis
-  proof 
+  proof
     show "0 \<in> U" ..
     show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" by (simp!)
     show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" by (simp!)
     show "\<forall>x \<in> U. - x = -#1 \<cdot> x" by (simp! add: negate_eq1)
-    show "\<forall>x \<in> U. \<forall>y \<in> U. x - y =  x + - y" 
+    show "\<forall>x \<in> U. \<forall>y \<in> U. x - y =  x + - y"
       by (simp! add: diff_eq1)
   qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+
 qed
 
 text {* The subspace relation is reflexive. *}
 
-lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V"
-proof 
+lemma subspace_refl [intro]: "is_vectorspace V \<Longrightarrow> is_subspace V V"
+proof
   assume "is_vectorspace V"
   show "0 \<in> V" ..
-  show "V <= V" ..
+  show "V \<subseteq> V" ..
   show "\<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V" by (simp!)
   show "\<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V" by (simp!)
 qed
 
 text {* The subspace relation is transitive. *}
 
-lemma subspace_trans: 
-  "[| is_subspace U V; is_vectorspace V; is_subspace V W |] 
-  ==> is_subspace U W"
-proof 
-  assume "is_subspace U V" "is_subspace V W" "is_vectorspace V"
+lemma subspace_trans:
+  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> is_subspace V W
+  \<Longrightarrow> is_subspace U W"
+proof
+  assume "is_subspace U V"  "is_subspace V W"  "is_vectorspace V"
   show "0 \<in> U" ..
 
-  have "U <= V" ..
-  also have "V <= W" ..
-  finally show "U <= W" .
+  have "U \<subseteq> V" ..
+  also have "V \<subseteq> W" ..
+  finally show "U \<subseteq> W" .
 
-  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" 
+  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U"
   proof (intro ballI)
-    fix x y assume "x \<in> U" "y \<in> U"
+    fix x y assume "x \<in> U"  "y \<in> U"
     show "x + y \<in> U" by (simp!)
   qed
 
@@ -134,12 +134,14 @@
 
 subsection {* Linear closure *}
 
-text {* The \emph{linear closure} of a vector $x$ is the set of all
-scalar multiples of $x$. *}
+text {*
+  The \emph{linear closure} of a vector @{text x} is the set of all
+  scalar multiples of @{text x}.
+*}
 
 constdefs
-  lin :: "('a::{minus,plus,zero}) => 'a set"
-  "lin x == {a \<cdot> x | a. True}" 
+  lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
+  "lin x \<equiv> {a \<cdot> x | a. True}"
 
 lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)"
   by (unfold lin_def) fast
@@ -149,59 +151,59 @@
 
 text {* Every vector is contained in its linear closure. *}
 
-lemma x_lin_x: "[| is_vectorspace V; x \<in> V |] ==> x \<in> lin x"
+lemma x_lin_x: "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x \<in> lin x"
 proof (unfold lin_def, intro CollectI exI conjI)
-  assume "is_vectorspace V" "x \<in> V"
+  assume "is_vectorspace V"  "x \<in> V"
   show "x = #1 \<cdot> x" by (simp!)
 qed simp
 
 text {* Any linear closure is a subspace. *}
 
-lemma lin_subspace [intro?]: 
-  "[| is_vectorspace V; x \<in> V |] ==> is_subspace (lin x) V"
+lemma lin_subspace [intro?]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> is_subspace (lin x) V"
 proof
-  assume "is_vectorspace V" "x \<in> V"
-  show "0 \<in> lin x" 
+  assume "is_vectorspace V"  "x \<in> V"
+  show "0 \<in> lin x"
   proof (unfold lin_def, intro CollectI exI conjI)
     show "0 = (#0::real) \<cdot> x" by (simp!)
   qed simp
 
-  show "lin x <= V"
-  proof (unfold lin_def, intro subsetI, elim CollectE exE conjE) 
-    fix xa a assume "xa = a \<cdot> x" 
+  show "lin x \<subseteq> V"
+  proof (unfold lin_def, intro subsetI, elim CollectE exE conjE)
+    fix xa a assume "xa = a \<cdot> x"
     show "xa \<in> V" by (simp!)
   qed
 
-  show "\<forall>x1 \<in> lin x. \<forall>x2 \<in> lin x. x1 + x2 \<in> lin x" 
+  show "\<forall>x1 \<in> lin x. \<forall>x2 \<in> lin x. x1 + x2 \<in> lin x"
   proof (intro ballI)
-    fix x1 x2 assume "x1 \<in> lin x" "x2 \<in> lin x" 
+    fix x1 x2 assume "x1 \<in> lin x"  "x2 \<in> lin x"
     thus "x1 + x2 \<in> lin x"
-    proof (unfold lin_def, elim CollectE exE conjE, 
+    proof (unfold lin_def, elim CollectE exE conjE,
       intro CollectI exI conjI)
-      fix a1 a2 assume "x1 = a1 \<cdot> x" "x2 = a2 \<cdot> x"
-      show "x1 + x2 = (a1 + a2) \<cdot> x" 
+      fix a1 a2 assume "x1 = a1 \<cdot> x"  "x2 = a2 \<cdot> x"
+      show "x1 + x2 = (a1 + a2) \<cdot> x"
         by (simp! add: vs_add_mult_distrib2)
     qed simp
   qed
 
-  show "\<forall>xa \<in> lin x. \<forall>a. a \<cdot> xa \<in> lin x" 
+  show "\<forall>xa \<in> lin x. \<forall>a. a \<cdot> xa \<in> lin x"
   proof (intro ballI allI)
-    fix x1 a assume "x1 \<in> lin x" 
+    fix x1 a assume "x1 \<in> lin x"
     thus "a \<cdot> x1 \<in> lin x"
     proof (unfold lin_def, elim CollectE exE conjE,
       intro CollectI exI conjI)
       fix a1 assume "x1 = a1 \<cdot> x"
       show "a \<cdot> x1 = (a * a1) \<cdot> x" by (simp!)
     qed simp
-  qed 
+  qed
 qed
 
 text {* Any linear closure is a vector space. *}
 
-lemma lin_vs [intro?]: 
-  "[| is_vectorspace V; x \<in> V |] ==> is_vectorspace (lin x)"
+lemma lin_vs [intro?]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> is_vectorspace (lin x)"
 proof (rule subspace_vs)
-  assume "is_vectorspace V" "x \<in> V"
+  assume "is_vectorspace V"  "x \<in> V"
   show "is_subspace (lin x) V" ..
 qed
 
@@ -209,49 +211,45 @@
 
 subsection {* Sum of two vectorspaces *}
 
-text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of
-all sums of elements from $U$ and $V$. *}
+text {*
+  The \emph{sum} of two vectorspaces @{text U} and @{text V} is the
+  set of all sums of elements from @{text U} and @{text V}.
+*}
 
 instance set :: (plus) plus ..
 
-defs vs_sum_def:
-  "U + V == {u + v | u v. u \<in> U \<and> v \<in> V}" (***
+defs (overloaded)
+  vs_sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}"
 
-constdefs 
-  vs_sum :: 
-  "['a::{plus, minus, zero} set, 'a set] => 'a set"         (infixl "+" 65)
-  "vs_sum U V == {x. \<exists>u \<in> U. \<exists>v \<in> V. x = u + v}";
-***)
-
-lemma vs_sumD: 
+lemma vs_sumD:
   "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
     by (unfold vs_sum_def) fast
 
 lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard]
 
-lemma vs_sumI [intro?]: 
-  "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
+lemma vs_sumI [intro?]:
+  "x \<in> U \<Longrightarrow> y \<in> V \<Longrightarrow> t = x + y \<Longrightarrow> t \<in> U + V"
   by (unfold vs_sum_def) fast
 
-text{* $U$ is a subspace of $U + V$. *}
+text {* @{text U} is a subspace of @{text "U + V"}. *}
 
-lemma subspace_vs_sum1 [intro?]: 
-  "[| is_vectorspace U; is_vectorspace V |]
-  ==> is_subspace U (U + V)"
-proof 
-  assume "is_vectorspace U" "is_vectorspace V"
+lemma subspace_vs_sum1 [intro?]:
+  "is_vectorspace U \<Longrightarrow> is_vectorspace V
+  \<Longrightarrow> is_subspace U (U + V)"
+proof
+  assume "is_vectorspace U"  "is_vectorspace V"
   show "0 \<in> U" ..
-  show "U <= U + V"
+  show "U \<subseteq> U + V"
   proof (intro subsetI vs_sumI)
   fix x assume "x \<in> U"
     show "x = x + 0" by (simp!)
     show "0 \<in> V" by (simp!)
   qed
-  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" 
+  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U"
   proof (intro ballI)
-    fix x y assume "x \<in> U" "y \<in> U" show "x + y \<in> U" by (simp!)
+    fix x y assume "x \<in> U"  "y \<in> U" show "x + y \<in> U" by (simp!)
   qed
-  show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" 
+  show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U"
   proof (intro ballI allI)
     fix x a assume "x \<in> U" show "a \<cdot> x \<in> U" by (simp!)
   qed
@@ -259,34 +257,34 @@
 
 text{* The sum of two subspaces is again a subspace.*}
 
-lemma vs_sum_subspace [intro?]: 
-  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
-  ==> is_subspace (U + V) E"
-proof 
-  assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"
+lemma vs_sum_subspace [intro?]:
+  "is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow> is_vectorspace E
+  \<Longrightarrow> is_subspace (U + V) E"
+proof
+  assume "is_subspace U E"  "is_subspace V E"  "is_vectorspace E"
   show "0 \<in> U + V"
   proof (intro vs_sumI)
     show "0 \<in> U" ..
     show "0 \<in> V" ..
     show "(0::'a) = 0 + 0" by (simp!)
   qed
-  
-  show "U + V <= E"
+
+  show "U + V \<subseteq> E"
   proof (intro subsetI, elim vs_sumE bexE)
-    fix x u v assume "u \<in> U" "v \<in> V" "x = u + v"
+    fix x u v assume "u \<in> U"  "v \<in> V"  "x = u + v"
     show "x \<in> E" by (simp!)
   qed
-  
+
   show "\<forall>x \<in> U + V. \<forall>y \<in> U + V. x + y \<in> U + V"
   proof (intro ballI)
-    fix x y assume "x \<in> U + V" "y \<in> U + V"
+    fix x y assume "x \<in> U + V"  "y \<in> U + V"
     thus "x + y \<in> U + V"
     proof (elim vs_sumE bexE, intro vs_sumI)
-      fix ux vx uy vy 
-      assume "ux \<in> U" "vx \<in> V" "x = ux + vx" 
-	and "uy \<in> U" "vy \<in> V" "y = uy + vy"
+      fix ux vx uy vy
+      assume "ux \<in> U"  "vx \<in> V"  "x = ux + vx"
+        and "uy \<in> U"  "vy \<in> V"  "y = uy + vy"
       show "x + y = (ux + uy) + (vx + vy)" by (simp!)
-    qed (simp!)+
+    qed (simp_all!)
   qed
 
   show "\<forall>x \<in> U + V. \<forall>a. a \<cdot> x \<in> U + V"
@@ -294,20 +292,20 @@
     fix x a assume "x \<in> U + V"
     thus "a \<cdot> x \<in> U + V"
     proof (elim vs_sumE bexE, intro vs_sumI)
-      fix a x u v assume "u \<in> U" "v \<in> V" "x = u + v"
-      show "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" 
+      fix a x u v assume "u \<in> U"  "v \<in> V"  "x = u + v"
+      show "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)"
         by (simp! add: vs_add_mult_distrib1)
-    qed (simp!)+
+    qed (simp_all!)
   qed
 qed
 
 text{* The sum of two subspaces is a vectorspace. *}
 
-lemma vs_sum_vs [intro?]: 
-  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
-  ==> is_vectorspace (U + V)"
+lemma vs_sum_vs [intro?]:
+  "is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow> is_vectorspace E
+  \<Longrightarrow> is_vectorspace (U + V)"
 proof (rule subspace_vs)
-  assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"
+  assume "is_subspace U E"  "is_subspace V E"  "is_vectorspace E"
   show "is_subspace (U + V) E" ..
 qed
 
@@ -316,28 +314,31 @@
 subsection {* Direct sums *}
 
 
-text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero 
-element is the only common element of $U$ and $V$. For every element
-$x$ of the direct sum of $U$ and $V$ the decomposition in
-$x = u + v$ with $u \in U$ and $v \in V$ is unique.*} 
+text {*
+  The sum of @{text U} and @{text V} is called \emph{direct}, iff the
+  zero element is the only common element of @{text U} and @{text
+  V}. For every element @{text x} of the direct sum of @{text U} and
+  @{text V} the decomposition in @{text "x = u + v"} with
+  @{text "u \<in> U"} and @{text "v \<in> V"} is unique.
+*}
 
-lemma decomp: 
-  "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
-  U \<inter> V = {0}; u1 \<in> U; u2 \<in> U; v1 \<in> V; v2 \<in> V; u1 + v1 = u2 + v2 |] 
-  ==> u1 = u2 \<and> v1 = v2" 
-proof 
-  assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  
-    "U \<inter> V = {0}" "u1 \<in> U" "u2 \<in> U" "v1 \<in> V" "v2 \<in> V" 
-    "u1 + v1 = u2 + v2" 
+lemma decomp:
+  "is_vectorspace E \<Longrightarrow> is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow>
+  U \<inter> V = {0} \<Longrightarrow> u1 \<in> U \<Longrightarrow> u2 \<in> U \<Longrightarrow> v1 \<in> V \<Longrightarrow> v2 \<in> V \<Longrightarrow>
+  u1 + v1 = u2 + v2 \<Longrightarrow> u1 = u2 \<and> v1 = v2"
+proof
+  assume "is_vectorspace E"  "is_subspace U E"  "is_subspace V E"
+    "U \<inter> V = {0}"  "u1 \<in> U"  "u2 \<in> U"  "v1 \<in> V"  "v2 \<in> V"
+    "u1 + v1 = u2 + v2"
   have eq: "u1 - u2 = v2 - v1" by (simp! add: vs_add_diff_swap)
-  have u: "u1 - u2 \<in> U" by (simp!) 
-  with eq have v': "v2 - v1 \<in> U" by simp 
-  have v: "v2 - v1 \<in> V" by (simp!) 
+  have u: "u1 - u2 \<in> U" by (simp!)
+  with eq have v': "v2 - v1 \<in> U" by simp
+  have v: "v2 - v1 \<in> V" by (simp!)
   with eq have u': "u1 - u2 \<in> V" by simp
-  
+
   show "u1 = u2"
   proof (rule vs_add_minus_eq)
-    show "u1 - u2 = 0" by (rule Int_singletonD [OF _ u u']) 
+    show "u1 - u2 = 0" by (rule Int_singletonD [OF _ u u'])
     show "u1 \<in> E" ..
     show "u2 \<in> E" ..
   qed
@@ -350,30 +351,33 @@
   qed
 qed
 
-text {* An application of the previous lemma will be used in the proof
-of the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
-element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and
-the linear closure of $x_0$ the components $y \in H$ and $a$ are
-uniquely determined. *}
+text {*
+  An application of the previous lemma will be used in the proof of
+  the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
+  element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a
+  vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"}
+  the components @{text "y \<in> H"} and @{text a} are uniquely
+  determined.
+*}
 
-lemma decomp_H': 
-  "[| is_vectorspace E; is_subspace H E; y1 \<in> H; y2 \<in> H; 
-  x' \<notin> H; x' \<in> E; x' \<noteq> 0; y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x' |]
-  ==> y1 = y2 \<and> a1 = a2"
+lemma decomp_H':
+  "is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow> y1 \<in> H \<Longrightarrow> y2 \<in> H \<Longrightarrow>
+  x' \<notin> H \<Longrightarrow> x' \<in> E \<Longrightarrow> x' \<noteq> 0 \<Longrightarrow> y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'
+  \<Longrightarrow> y1 = y2 \<and> a1 = a2"
 proof
   assume "is_vectorspace E" and h: "is_subspace H E"
-     and "y1 \<in> H" "y2 \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" 
+     and "y1 \<in> H"  "y2 \<in> H"  "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
          "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
 
   have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
-  proof (rule decomp) 
-    show "a1 \<cdot> x' \<in> lin x'" .. 
+  proof (rule decomp)
+    show "a1 \<cdot> x' \<in> lin x'" ..
     show "a2 \<cdot> x' \<in> lin x'" ..
-    show "H \<inter> (lin x') = {0}" 
+    show "H \<inter> (lin x') = {0}"
     proof
-      show "H \<inter> lin x' <= {0}" 
+      show "H \<inter> lin x' \<subseteq> {0}"
       proof (intro subsetI, elim IntE, rule singleton_iff [THEN iffD2])
-        fix x assume "x \<in> H" "x \<in> lin x'" 
+        fix x assume "x \<in> H"  "x \<in> lin x'"
         thus "x = 0"
         proof (unfold lin_def, elim CollectE exE conjE)
           fix a assume "x = a \<cdot> x'"
@@ -381,8 +385,8 @@
           proof cases
             assume "a = (#0::real)" show ?thesis by (simp!)
           next
-            assume "a \<noteq> (#0::real)" 
-            from h have "inverse a \<cdot> a \<cdot> x' \<in> H" 
+            assume "a \<noteq> (#0::real)"
+            from h have "inverse a \<cdot> a \<cdot> x' \<in> H"
               by (rule subspace_mult_closed) (simp!)
             also have "inverse a \<cdot> a \<cdot> x' = x'" by (simp!)
             finally have "x' \<in> H" .
@@ -390,87 +394,91 @@
           qed
        qed
       qed
-      show "{0} <= H \<inter> lin x'"
+      show "{0} \<subseteq> H \<inter> lin x'"
       proof -
-	have "0 \<in> H \<inter> lin x'"
-	proof (rule IntI)
-	  show "0 \<in> H" ..
-	  from lin_vs show "0 \<in> lin x'" ..
-	qed
-	thus ?thesis by simp
+        have "0 \<in> H \<inter> lin x'"
+        proof (rule IntI)
+          show "0 \<in> H" ..
+          from lin_vs show "0 \<in> lin x'" ..
+        qed
+        thus ?thesis by simp
       qed
     qed
     show "is_subspace (lin x') E" ..
   qed
-  
+
   from c show "y1 = y2" by simp
-  
-  show  "a1 = a2" 
+
+  show  "a1 = a2"
   proof (rule vs_mult_right_cancel [THEN iffD1])
     from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp
   qed
 qed
 
-text {* Since for any element $y + a \mult x'$ of the direct sum 
-of a vectorspace $H$ and the linear closure of $x'$ the components
-$y\in H$ and $a$ are unique, it follows from $y\in H$ that 
-$a = 0$.*} 
+text {*
+  Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a
+  vectorspace @{text H} and the linear closure of @{text x'} the
+  components @{text "y \<in> H"} and @{text a} are unique, it follows from
+  @{text "y \<in> H"} that @{text "a = 0"}.
+*}
 
-lemma decomp_H'_H: 
-  "[| is_vectorspace E; is_subspace H E; t \<in> H; x' \<notin> H; x' \<in> E;
-  x' \<noteq> 0 |] 
-  ==> (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, (#0::real))"
+lemma decomp_H'_H:
+  "is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow> t \<in> H \<Longrightarrow> x' \<notin> H \<Longrightarrow> x' \<in> E
+  \<Longrightarrow> x' \<noteq> 0
+  \<Longrightarrow> (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, (#0::real))"
 proof (rule, unfold split_tupled_all)
-  assume "is_vectorspace E" "is_subspace H E" "t \<in> H" "x' \<notin> H" "x' \<in> E"
+  assume "is_vectorspace E"  "is_subspace H E"  "t \<in> H"  "x' \<notin> H"  "x' \<in> E"
     "x' \<noteq> 0"
   have h: "is_vectorspace H" ..
   fix y a presume t1: "t = y + a \<cdot> x'" and "y \<in> H"
-  have "y = t \<and> a = (#0::real)" 
-    by (rule decomp_H') (assumption | (simp!))+
+  have "y = t \<and> a = (#0::real)"
+    by (rule decomp_H') (auto!)
   thus "(y, a) = (t, (#0::real))" by (simp!)
-qed (simp!)+
+qed (simp_all!)
 
-text {* The components $y\in H$ and $a$ in $y \plus a \mult x'$ 
-are unique, so the function $h'$ defined by 
-$h' (y \plus a \mult x') = h y + a \cdot \xi$ is definite. *}
+text {*
+  The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}
+  are unique, so the function @{text h'} defined by
+  @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite.
+*}
 
 lemma h'_definite:
-  "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
-                in (h y) + a * xi);
-  x = y + a \<cdot> x'; is_vectorspace E; is_subspace H E;
-  y \<in> H; x' \<notin> H; x' \<in> E; x' \<noteq> 0 |]
-  ==> h' x = h y + a * xi"
-proof -  
-  assume 
-    "h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
+  "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
+                in (h y) + a * xi) \<Longrightarrow>
+  x = y + a \<cdot> x' \<Longrightarrow> is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow>
+  y \<in> H \<Longrightarrow> x' \<notin> H \<Longrightarrow> x' \<in> E \<Longrightarrow> x' \<noteq> 0
+  \<Longrightarrow> h' x = h y + a * xi"
+proof -
+  assume
+    "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
                in (h y) + a * xi)"
-    "x = y + a \<cdot> x'" "is_vectorspace E" "is_subspace H E"
-    "y \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
-  have "x \<in> H + (lin x')" 
-    by (simp! add: vs_sum_def lin_def) force+
-  have "\<exists>! xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)" 
+    "x = y + a \<cdot> x'"  "is_vectorspace E"  "is_subspace H E"
+    "y \<in> H"  "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
+  hence "x \<in> H + (lin x')"
+    by (auto simp add: vs_sum_def lin_def)
+  have "\<exists>! xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)"
   proof
     show "\<exists>xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)"
-      by (force!)
+      by (blast!)
   next
     fix xa ya
     assume "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) xa"
            "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) ya"
-    show "xa = ya" 
+    show "xa = ya"
     proof -
-      show "fst xa = fst ya \<and> snd xa = snd ya ==> xa = ya" 
+      show "fst xa = fst ya \<and> snd xa = snd ya \<Longrightarrow> xa = ya"
         by (simp add: Pair_fst_snd_eq)
-      have x: "x = fst xa + snd xa \<cdot> x' \<and> fst xa \<in> H" 
-        by (force!)
-      have y: "x = fst ya + snd ya \<cdot> x' \<and> fst ya \<in> H" 
-        by (force!)
-      from x y show "fst xa = fst ya \<and> snd xa = snd ya" 
+      have x: "x = fst xa + snd xa \<cdot> x' \<and> fst xa \<in> H"
+        by (auto!)
+      have y: "x = fst ya + snd ya \<cdot> x' \<and> fst ya \<in> H"
+        by (auto!)
+      from x y show "fst xa = fst ya \<and> snd xa = snd ya"
         by (elim conjE) (rule decomp_H', (simp!)+)
     qed
   qed
-  hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" 
-    by (rule some1_equality) (force!)
+  hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"
+    by (rule some1_equality) (blast!)
   thus "h' x = h y + a * xi" by (simp! add: Let_def)
 qed
 
-end
\ No newline at end of file
+end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -9,127 +9,124 @@
 
 subsection {* Signature *}
 
-text {* For the definition of real vector spaces a type $\alpha$
-of the sort $\{ \idt{plus}, \idt{minus}, \idt{zero}\}$ is considered, on which a
-real scalar multiplication $\mult$ is defined. *}
+text {*
+  For the definition of real vector spaces a type @{typ 'a} of the
+  sort @{text "{plus, minus, zero}"} is considered, on which a real
+  scalar multiplication @{text \<cdot>} is declared.
+*}
 
 consts
-  prod  :: "[real, 'a::{plus, minus, zero}] => 'a"     (infixr "'(*')" 70)
+  prod  :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a"     (infixr "'(*')" 70)
 
 syntax (symbols)
-  prod  :: "[real, 'a] => 'a"                          (infixr "\<cdot>" 70)
+  prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 70)
 
 
 subsection {* Vector space laws *}
 
-text {* A \emph{vector space} is a non-empty set $V$ of elements from
-  $\alpha$ with the following vector space laws: The set $V$ is closed
-  under addition and scalar multiplication, addition is associative
-  and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
-  and $0$ is the neutral element of addition.  Addition and
-  multiplication are distributive; scalar multiplication is
-  associative and the real number $1$ is the neutral element of scalar
-  multiplication.
+text {*
+  A \emph{vector space} is a non-empty set @{text V} of elements from
+  @{typ 'a} with the following vector space laws: The set @{text V} is
+  closed under addition and scalar multiplication, addition is
+  associative and commutative; @{text "- x"} is the inverse of @{text
+  x} w.~r.~t.~addition and @{text 0} is the neutral element of
+  addition.  Addition and multiplication are distributive; scalar
+  multiplication is associative and the real number @{text "#1"} is
+  the neutral element of scalar multiplication.
 *}
 
 constdefs
-  is_vectorspace :: "('a::{plus, minus, zero}) set => bool"
-  "is_vectorspace V == V \<noteq> {}
+  is_vectorspace :: "('a::{plus, minus, zero}) set \<Rightarrow> bool"
+  "is_vectorspace V \<equiv> V \<noteq> {}
    \<and> (\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. \<forall>a b.
-        x + y \<in> V                                 
-      \<and> a \<cdot> x \<in> V                                 
-      \<and> (x + y) + z = x + (y + z)             
-      \<and> x + y = y + x                           
-      \<and> x - x = 0                               
-      \<and> 0 + x = x                               
-      \<and> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y       
-      \<and> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x         
-      \<and> (a * b) \<cdot> x = a \<cdot> b \<cdot> x               
+        x + y \<in> V
+      \<and> a \<cdot> x \<in> V
+      \<and> (x + y) + z = x + (y + z)
+      \<and> x + y = y + x
+      \<and> x - x = 0
+      \<and> 0 + x = x
+      \<and> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y
+      \<and> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x
+      \<and> (a * b) \<cdot> x = a \<cdot> b \<cdot> x
       \<and> #1 \<cdot> x = x
       \<and> - x = (- #1) \<cdot> x
-      \<and> x - y = x + - y)"                             
+      \<and> x - y = x + - y)"
 
-text_raw {* \medskip *}
-text {* The corresponding introduction rule is:*}
+
+text {* \medskip The corresponding introduction rule is:*}
 
 lemma vsI [intro]:
-  "[| 0 \<in> V; 
-  \<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V; 
-  \<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V;  
-  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. (x + y) + z = x + (y + z);
-  \<forall>x \<in> V. \<forall>y \<in> V. x + y = y + x;
-  \<forall>x \<in> V. x - x = 0;
-  \<forall>x \<in> V. 0 + x = x;
-  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a. a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y;
-  \<forall>x \<in> V. \<forall>a b. (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x;
-  \<forall>x \<in> V. \<forall>a b. (a * b) \<cdot> x = a \<cdot> b \<cdot> x; 
-  \<forall>x \<in> V. #1 \<cdot> x = x; 
-  \<forall>x \<in> V. - x = (- #1) \<cdot> x; 
-  \<forall>x \<in> V. \<forall>y \<in> V. x - y = x + - y |] ==> is_vectorspace V"
-proof (unfold is_vectorspace_def, intro conjI ballI allI)
-  fix x y z 
-  assume "x \<in> V" "y \<in> V" "z \<in> V"
-    "\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. x + y + z = x + (y + z)"
-  thus "x + y + z =  x + (y + z)" by blast
-qed force+
+  "0 \<in> V \<Longrightarrow>
+  \<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V \<Longrightarrow>
+  \<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V \<Longrightarrow>
+  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. (x + y) + z = x + (y + z) \<Longrightarrow>
+  \<forall>x \<in> V. \<forall>y \<in> V. x + y = y + x \<Longrightarrow>
+  \<forall>x \<in> V. x - x = 0 \<Longrightarrow>
+  \<forall>x \<in> V. 0 + x = x \<Longrightarrow>
+  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a. a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y \<Longrightarrow>
+  \<forall>x \<in> V. \<forall>a b. (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x \<Longrightarrow>
+  \<forall>x \<in> V. \<forall>a b. (a * b) \<cdot> x = a \<cdot> b \<cdot> x \<Longrightarrow>
+  \<forall>x \<in> V. #1 \<cdot> x = x \<Longrightarrow>
+  \<forall>x \<in> V. - x = (- #1) \<cdot> x \<Longrightarrow>
+  \<forall>x \<in> V. \<forall>y \<in> V. x - y = x + - y \<Longrightarrow> is_vectorspace V"
+  by (unfold is_vectorspace_def) auto
 
-text_raw {* \medskip *}
-text {* The corresponding destruction rules are: *}
+text {* \medskip The corresponding destruction rules are: *}
 
-lemma negate_eq1: 
-  "[| is_vectorspace V; x \<in> V |] ==> - x = (- #1) \<cdot> x"
+lemma negate_eq1:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - x = (- #1) \<cdot> x"
+  by (unfold is_vectorspace_def) simp
+
+lemma diff_eq1:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y"
   by (unfold is_vectorspace_def) simp
 
-lemma diff_eq1: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y = x + - y"
-  by (unfold is_vectorspace_def) simp 
+lemma negate_eq2:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- #1) \<cdot> x = - x"
+  by (unfold is_vectorspace_def) simp
 
-lemma negate_eq2: 
-  "[| is_vectorspace V; x \<in> V |] ==> (- #1) \<cdot> x = - x"
+lemma negate_eq2a:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> #-1 \<cdot> x = - x"
   by (unfold is_vectorspace_def) simp
 
-lemma negate_eq2a: 
-  "[| is_vectorspace V; x \<in> V |] ==> #-1 \<cdot> x = - x"
+lemma diff_eq2:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"
+  by (unfold is_vectorspace_def) simp
+
+lemma vs_not_empty [intro?]: "is_vectorspace V \<Longrightarrow> (V \<noteq> {})"
   by (unfold is_vectorspace_def) simp
 
-lemma diff_eq2: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + - y = x - y"
-  by (unfold is_vectorspace_def) simp  
+lemma vs_add_closed [simp, intro?]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
+  by (unfold is_vectorspace_def) simp
 
-lemma vs_not_empty [intro?]: "is_vectorspace V ==> (V \<noteq> {})" 
-  by (unfold is_vectorspace_def) simp
- 
-lemma vs_add_closed [simp, intro?]: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + y \<in> V" 
+lemma vs_mult_closed [simp, intro?]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
   by (unfold is_vectorspace_def) simp
 
-lemma vs_mult_closed [simp, intro?]: 
-  "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> x \<in> V" 
-  by (unfold is_vectorspace_def) simp
-
-lemma vs_diff_closed [simp, intro?]: 
- "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y \<in> V"
+lemma vs_diff_closed [simp, intro?]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"
   by (simp add: diff_eq1 negate_eq1)
 
-lemma vs_neg_closed  [simp, intro?]: 
-  "[| is_vectorspace V; x \<in> V |] ==> - x \<in> V"
+lemma vs_neg_closed  [simp, intro?]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - x \<in> V"
   by (simp add: negate_eq1)
 
-lemma vs_add_assoc [simp]:  
-  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
-   ==> (x + y) + z = x + (y + z)"
-  by (unfold is_vectorspace_def) fast
+lemma vs_add_assoc [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+   \<Longrightarrow> (x + y) + z = x + (y + z)"
+  by (unfold is_vectorspace_def) blast
 
-lemma vs_add_commute [simp]: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> y + x = x + y"
-  by (unfold is_vectorspace_def) simp
+lemma vs_add_commute [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> y + x = x + y"
+  by (unfold is_vectorspace_def) blast
 
 lemma vs_add_left_commute [simp]:
-  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
-  ==> x + (y + z) = y + (x + z)"
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+  \<Longrightarrow> x + (y + z) = y + (x + z)"
 proof -
-  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
-  hence "x + (y + z) = (x + y) + z" 
+  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "z \<in> V"
+  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)
@@ -138,94 +135,93 @@
 
 theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute
 
-lemma vs_diff_self [simp]: 
-  "[| is_vectorspace V; x \<in> V |] ==>  x - x = 0" 
+lemma vs_diff_self [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x - x = 0"
   by (unfold is_vectorspace_def) simp
 
 text {* The existence of the zero element of a vector space
 follows from the non-emptiness of carrier set. *}
 
-lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \<in> V"
-proof - 
+lemma zero_in_vs [simp, intro]: "is_vectorspace V \<Longrightarrow> 0 \<in> V"
+proof -
   assume "is_vectorspace V"
   have "V \<noteq> {}" ..
-  hence "\<exists>x. x \<in> V" by force
-  thus ?thesis 
-  proof 
-    fix x assume "x \<in> V" 
+  hence "\<exists>x. x \<in> V" by blast
+  thus ?thesis
+  proof
+    fix x assume "x \<in> V"
     have "0 = x - x" by (simp!)
     also have "... \<in> V" by (simp! only: vs_diff_closed)
     finally show ?thesis .
   qed
 qed
 
-lemma vs_add_zero_left [simp]: 
-  "[| is_vectorspace V; x \<in> V |] ==>  0 + x = x"
+lemma vs_add_zero_left [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow>  0 + x = x"
   by (unfold is_vectorspace_def) simp
 
-lemma vs_add_zero_right [simp]: 
-  "[| is_vectorspace V; x \<in> V |] ==>  x + 0 = x"
+lemma vs_add_zero_right [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow>  x + 0 = x"
 proof -
-  assume "is_vectorspace V" "x \<in> V"
+  assume "is_vectorspace V"  "x \<in> V"
   hence "x + 0 = 0 + x" by simp
   also have "... = x" by (simp!)
   finally show ?thesis .
 qed
 
-lemma vs_add_mult_distrib1: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
-  ==> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
+lemma vs_add_mult_distrib1:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
+  \<Longrightarrow> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
   by (unfold is_vectorspace_def) simp
 
-lemma vs_add_mult_distrib2: 
-  "[| is_vectorspace V; x \<in> V |] 
-  ==> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" 
+lemma vs_add_mult_distrib2:
+  "is_vectorspace V \<Longrightarrow> x \<in> V
+  \<Longrightarrow> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"
   by (unfold is_vectorspace_def) simp
 
-lemma vs_mult_assoc: 
-  "[| is_vectorspace V; x \<in> V |] ==> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
+lemma vs_mult_assoc:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
   by (unfold is_vectorspace_def) simp
 
-lemma vs_mult_assoc2 [simp]: 
- "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
+lemma vs_mult_assoc2 [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
   by (simp only: vs_mult_assoc)
 
-lemma vs_mult_1 [simp]: 
-  "[| is_vectorspace V; x \<in> V |] ==> #1 \<cdot> x = x" 
+lemma vs_mult_1 [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> #1 \<cdot> x = x"
   by (unfold is_vectorspace_def) simp
 
-lemma vs_diff_mult_distrib1: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
-  ==> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
+lemma vs_diff_mult_distrib1:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
+  \<Longrightarrow> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
   by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1)
 
-lemma vs_diff_mult_distrib2: 
-  "[| is_vectorspace V; x \<in> V |] 
-  ==> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
+lemma vs_diff_mult_distrib2:
+  "is_vectorspace V \<Longrightarrow> x \<in> V
+  \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
 proof -
-  assume "is_vectorspace V" "x \<in> V"
-  have " (a - b) \<cdot> x = (a + - b) \<cdot> x" 
+  assume "is_vectorspace V"  "x \<in> V"
+  have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
     by (unfold real_diff_def, simp)
-  also have "... = a \<cdot> x + (- b) \<cdot> x" 
+  also have "... = a \<cdot> x + (- b) \<cdot> x"
     by (rule vs_add_mult_distrib2)
-  also have "... = a \<cdot> x + - (b \<cdot> x)" 
+  also have "... = a \<cdot> x + - (b \<cdot> x)"
     by (simp! add: negate_eq1)
-  also have "... = a \<cdot> x - (b \<cdot> x)" 
+  also have "... = a \<cdot> x - (b \<cdot> x)"
     by (simp! add: diff_eq1)
   finally show ?thesis .
 qed
 
-(*text_raw {* \paragraph {Further derived laws.} *}*)
-text_raw {* \medskip *}
-text{* Further derived laws: *}
+
+text {* \medskip Further derived laws: *}
 
-lemma vs_mult_zero_left [simp]: 
-  "[| is_vectorspace V; x \<in> V |] ==> #0 \<cdot> x = 0"
+lemma vs_mult_zero_left [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> #0 \<cdot> x = 0"
 proof -
-  assume "is_vectorspace V" "x \<in> V"
+  assume "is_vectorspace V"  "x \<in> V"
   have  "#0 \<cdot> x = (#1 - #1) \<cdot> x" by simp
   also have "... = (#1 + - #1) \<cdot> x" by simp
-  also have "... =  #1 \<cdot> x + (- #1) \<cdot> x" 
+  also have "... =  #1 \<cdot> x + (- #1) \<cdot> x"
     by (rule vs_add_mult_distrib2)
   also have "... = x + (- #1) \<cdot> x" by (simp!)
   also have "... = x + - x" by (simp! add: negate_eq2a)
@@ -234,9 +230,9 @@
   finally show ?thesis .
 qed
 
-lemma vs_mult_zero_right [simp]: 
-  "[| is_vectorspace (V:: 'a::{plus, minus, zero} set) |] 
-  ==> a \<cdot> 0 = (0::'a)"
+lemma vs_mult_zero_right [simp]:
+  "is_vectorspace (V:: 'a::{plus, minus, zero} set)
+  \<Longrightarrow> a \<cdot> 0 = (0::'a)"
 proof -
   assume "is_vectorspace V"
   have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by (simp!)
@@ -246,41 +242,41 @@
   finally show ?thesis .
 qed
 
-lemma vs_minus_mult_cancel [simp]:  
-  "[| is_vectorspace V; x \<in> V |] ==> (- a) \<cdot> - x = a \<cdot> x"
+lemma vs_minus_mult_cancel [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"
   by (simp add: negate_eq1)
 
-lemma vs_add_minus_left_eq_diff: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + y = y - x"
-proof - 
-  assume "is_vectorspace V" "x \<in> V" "y \<in> V"
-  hence "- x + y = y + - x" 
+lemma vs_add_minus_left_eq_diff:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
+proof -
+  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"
+  hence "- x + y = y + - x"
     by (simp add: vs_add_commute)
   also have "... = y - x" by (simp! add: diff_eq1)
   finally show ?thesis .
 qed
 
-lemma vs_add_minus [simp]: 
-  "[| is_vectorspace V; x \<in> V |] ==> x + - x = 0"
+lemma vs_add_minus [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x + - x = 0"
   by (simp! add: diff_eq2)
 
-lemma vs_add_minus_left [simp]: 
-  "[| is_vectorspace V; x \<in> V |] ==> - x + x = 0"
+lemma vs_add_minus_left [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - x + x = 0"
   by (simp! add: diff_eq2)
 
-lemma vs_minus_minus [simp]: 
-  "[| is_vectorspace V; x \<in> V |] ==> - (- x) = x"
+lemma vs_minus_minus [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - (- x) = x"
   by (simp add: negate_eq1)
 
-lemma vs_minus_zero [simp]: 
-  "is_vectorspace (V::'a::{plus, minus, zero} set) ==> - (0::'a) = 0" 
+lemma vs_minus_zero [simp]:
+  "is_vectorspace (V::'a::{plus, minus, zero} set) \<Longrightarrow> - (0::'a) = 0"
   by (simp add: negate_eq1)
 
 lemma vs_minus_zero_iff [simp]:
-  "[| is_vectorspace V; x \<in> V |] ==> (- x = 0) = (x = 0)" 
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- x = 0) = (x = 0)"
   (concl is "?L = ?R")
 proof -
-  assume "is_vectorspace V" "x \<in> V"
+  assume "is_vectorspace V"  "x \<in> V"
   show "?L = ?R"
   proof
     have "x = - (- x)" by (simp! add: vs_minus_minus)
@@ -290,81 +286,81 @@
   qed (simp!)
 qed
 
-lemma vs_add_minus_cancel [simp]:  
-  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + (- x + y) = y" 
-  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute) 
+lemma vs_add_minus_cancel [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y"
+  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute)
 
-lemma vs_minus_add_cancel [simp]: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + (x + y) = y" 
-  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute) 
+lemma vs_minus_add_cancel [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + (x + y) = y"
+  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute)
 
-lemma vs_minus_add_distrib [simp]:  
-  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
-  ==> - (x + y) = - x + - y"
+lemma vs_minus_add_distrib [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
+  \<Longrightarrow> - (x + y) = - x + - y"
   by (simp add: negate_eq1 vs_add_mult_distrib1)
 
-lemma vs_diff_zero [simp]: 
-  "[| is_vectorspace V; x \<in> V |] ==> x - 0 = x"
-  by (simp add: diff_eq1)  
+lemma vs_diff_zero [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x - 0 = x"
+  by (simp add: diff_eq1)
 
-lemma vs_diff_zero_right [simp]: 
-  "[| is_vectorspace V; x \<in> V |] ==> 0 - x = - x"
+lemma vs_diff_zero_right [simp]:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> 0 - x = - x"
   by (simp add:diff_eq1)
 
 lemma vs_add_left_cancel:
-  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
-   ==> (x + y = x + z) = (y = z)"  
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+   \<Longrightarrow> (x + y = x + z) = (y = z)"
   (concl is "?L = ?R")
 proof
-  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
+  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "z \<in> V"
   have "y = 0 + y" by (simp!)
   also have "... = - x + x + y" by (simp!)
-  also have "... = - x + (x + y)" 
+  also have "... = - x + (x + y)"
     by (simp! only: vs_add_assoc vs_neg_closed)
   also assume "x + y = x + z"
-  also have "- x + (x + z) = - x + x + z" 
+  also have "- x + (x + z) = - x + x + z"
     by (simp! only: vs_add_assoc [symmetric] vs_neg_closed)
   also have "... = z" by (simp!)
   finally show ?R .
-qed force
+qed blast
 
-lemma vs_add_right_cancel: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
-  ==> (y + x = z + x) = (y = z)"  
+lemma vs_add_right_cancel:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+  \<Longrightarrow> (y + x = z + x) = (y = z)"
   by (simp only: vs_add_commute vs_add_left_cancel)
 
-lemma vs_add_assoc_cong: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V; x' \<in> V; y' \<in> V; z \<in> V |] 
-  ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"
-  by (simp only: vs_add_assoc [symmetric]) 
+lemma vs_add_assoc_cong:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V
+  \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"
+  by (simp only: vs_add_assoc [symmetric])
 
-lemma vs_mult_left_commute: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
-  ==> x \<cdot> y \<cdot> z = y \<cdot> x \<cdot> z"  
+lemma vs_mult_left_commute:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+  \<Longrightarrow> x \<cdot> y \<cdot> z = y \<cdot> x \<cdot> z"
   by (simp add: real_mult_commute)
 
 lemma vs_mult_zero_uniq:
-  "[| is_vectorspace V; x \<in> V; x \<noteq> 0; a \<cdot> x = 0 |] ==> a = 0"
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0"
 proof (rule classical)
-  assume "is_vectorspace V" "x \<in> V" "a \<cdot> x = 0" "x \<noteq> 0"
+  assume "is_vectorspace V"  "x \<in> V"  "a \<cdot> x = 0"  "x \<noteq> 0"
   assume "a \<noteq> 0"
   have "x = (inverse a * a) \<cdot> x" by (simp!)
   also have "... = inverse a \<cdot> (a \<cdot> x)" by (rule vs_mult_assoc)
   also have "... = inverse a \<cdot> 0" by (simp!)
   also have "... = 0" by (simp!)
   finally have "x = 0" .
-  thus "a = 0" by contradiction 
+  thus "a = 0" by contradiction
 qed
 
-lemma vs_mult_left_cancel: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V; a \<noteq> #0 |] ==> 
+lemma vs_mult_left_cancel:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<noteq> #0 \<Longrightarrow>
   (a \<cdot> x = a \<cdot> y) = (x = y)"
   (concl is "?L = ?R")
 proof
-  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "a \<noteq> #0"
+  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "a \<noteq> #0"
   have "x = #1 \<cdot> x" by (simp!)
   also have "... = (inverse a * a) \<cdot> x" by (simp!)
-  also have "... = inverse a \<cdot> (a \<cdot> x)" 
+  also have "... = inverse a \<cdot> (a \<cdot> x)"
     by (simp! only: vs_mult_assoc)
   also assume ?L
   also have "inverse a \<cdot> ... = y" by (simp!)
@@ -372,51 +368,51 @@
 qed simp
 
 lemma vs_mult_right_cancel: (*** forward ***)
-  "[| is_vectorspace V; x \<in> V; x \<noteq> 0 |] 
-  ==> (a \<cdot> x = b \<cdot> x) = (a = b)" (concl is "?L = ?R")
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x \<noteq> 0
+  \<Longrightarrow> (a \<cdot> x = b \<cdot> x) = (a = b)" (concl is "?L = ?R")
 proof
-  assume v: "is_vectorspace V" "x \<in> V" "x \<noteq> 0"
-  have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x" 
+  assume v: "is_vectorspace V"  "x \<in> V"  "x \<noteq> 0"
+  have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"
     by (simp! add: vs_diff_mult_distrib2)
   also assume ?L hence "a \<cdot> x - b \<cdot> x = 0" by (simp!)
   finally have "(a - b) \<cdot> x = 0" .
-  from v this have "a - b = 0" by (rule vs_mult_zero_uniq) 
+  from v this have "a - b = 0" by (rule vs_mult_zero_uniq)
   thus "a = b" by simp
-qed simp 
+qed simp
 
-lemma vs_eq_diff_eq: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] ==> 
+lemma vs_eq_diff_eq:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow>
   (x = z - y) = (x + y = z)"
-  (concl is "?L = ?R" )  
+  (concl is "?L = ?R" )
 proof -
-  assume vs: "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
-  show "?L = ?R"   
+  assume vs: "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "z \<in> V"
+  show "?L = ?R"
   proof
     assume ?L
     hence "x + y = z - y + y" by simp
     also have "... = z + - y + y" by (simp! add: diff_eq1)
-    also have "... = z + (- y + y)" 
+    also have "... = z + (- y + y)"
       by (rule vs_add_assoc) (simp!)+
-    also from vs have "... = z + 0" 
+    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
     hence "z - y = (x + y) - y" by simp
-    also from vs have "... = x + y + - y" 
+    also from vs have "... = x + y + - y"
       by (simp add: diff_eq1)
-    also have "... = x + (y + - y)" 
+    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 \<in> V; y \<in> V; x + y = 0 |] ==> x = - y" 
+lemma vs_add_minus_eq_minus:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = 0 \<Longrightarrow> x = - y"
 proof -
-  assume "is_vectorspace V" "x \<in> V" "y \<in> V" 
+  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"
   have "x = (- y + y) + x" by (simp!)
   also have "... = - y + (x + y)" by (simp!)
   also assume "x + y = 0"
@@ -424,41 +420,41 @@
   finally show "x = - y" .
 qed
 
-lemma vs_add_minus_eq: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V; x - y = 0 |] ==> x = y" 
+lemma vs_add_minus_eq:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = 0 \<Longrightarrow> x = y"
 proof -
-  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "x - y = 0"
+  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "x - y = 0"
   assume "x - y = 0"
   hence e: "x + - y = 0" by (simp! add: diff_eq1)
-  with _ _ _ have "x = - (- y)" 
+  with _ _ _ have "x = - (- y)"
     by (rule vs_add_minus_eq_minus) (simp!)+
   thus "x = y" by (simp!)
 qed
 
 lemma vs_add_diff_swap:
-  "[| is_vectorspace V; a \<in> V; b \<in> V; c \<in> V; d \<in> V; a + b = c + d |] 
-  ==> a - c = d - b"
-proof - 
-  assume vs: "is_vectorspace V" "a \<in> V" "b \<in> V" "c \<in> V" "d \<in> V" 
+  "is_vectorspace V \<Longrightarrow> a \<in> V \<Longrightarrow> b \<in> V \<Longrightarrow> c \<in> V \<Longrightarrow> d \<in> V \<Longrightarrow> a + b = c + d
+  \<Longrightarrow> a - c = d - b"
+proof -
+  assume vs: "is_vectorspace V"  "a \<in> V"  "b \<in> V"  "c \<in> V"  "d \<in> V"
     and eq: "a + b = c + d"
-  have "- c + (a + b) = - c + (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" 
+  from vs have "a - c = (- c + (a + b)) + - b"
     by (simp add: vs_add_ac diff_eq1)
-  also from eq have "...  = d + - b" 
+  also from eq have "...  = d + - b"
     by (simp! add: vs_add_right_cancel)
   also have "... = d - b" by (simp! add: diff_eq2)
   finally show "a - c = d - b" .
 qed
 
-lemma vs_add_cancel_21: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V; u \<in> V |] 
-  ==> (x + (y + z) = y + u) = ((x + z) = u)"
-  (concl is "?L = ?R") 
-proof - 
-  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V"
+lemma vs_add_cancel_21:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> u \<in> V
+  \<Longrightarrow> (x + (y + z) = y + u) = ((x + z) = u)"
+  (concl is "?L = ?R")
+proof -
+  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "z \<in> V"  "u \<in> V"
   show "?L = ?R"
   proof
     have "x + z = - y + y + (x + z)" by (simp!)
@@ -471,16 +467,16 @@
   qed (simp! only: vs_add_left_commute [of V x])
 qed
 
-lemma vs_add_cancel_end: 
-  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
-  ==> (x + (y + z) = y) = (x = - z)"
+lemma vs_add_cancel_end:
+  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+  \<Longrightarrow> (x + (y + z) = y) = (x = - z)"
   (concl is "?L = ?R" )
 proof -
-  assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
+  assume "is_vectorspace V"  "x \<in> V"  "y \<in> V"  "z \<in> V"
   show "?L = ?R"
   proof
     assume l: ?L
-    have "x + z = 0" 
+    have "x + z = 0"
     proof (rule vs_add_left_cancel [THEN iffD1])
       have "y + (x + z) = x + (y + z)" by (simp!)
       also note l
@@ -490,12 +486,12 @@
     thus "x = - z" by (simp! add: vs_add_minus_eq_minus)
   next
     assume r: ?R
-    hence "x + (y + z) = - z + (y + z)" by simp 
-    also have "... = y + (- z + z)" 
+    hence "x + (y + z) = - z + (y + z)" by simp
+    also have "... = y + (- z + z)"
       by (simp! only: vs_add_left_commute)
     also have "... = y"  by (simp!)
     finally show ?L .
   qed
 qed
 
-end
\ No newline at end of file
+end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/ZornLemma.thy
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Sat Dec 16 21:41:51 2000 +0100
@@ -7,49 +7,52 @@
 
 theory ZornLemma = Aux + Zorn:
 
-text {* Zorn's Lemmas states: if every linear ordered subset of an
-ordered set $S$ has an upper bound in $S$, then there exists a maximal
-element in $S$.  In our application, $S$ is a set of sets ordered by
-set inclusion. Since the union of a chain of sets is an upper bound
-for all elements of the chain, the conditions of Zorn's lemma can be
-modified: if $S$ is non-empty, it suffices to show that for every
-non-empty chain $c$ in $S$ the union of $c$ also lies in $S$. *}
+text {*
+  Zorn's Lemmas states: if every linear ordered subset of an ordered
+  set @{text S} has an upper bound in @{text S}, then there exists a
+  maximal element in @{text S}.  In our application, @{text S} is a
+  set of sets ordered by set inclusion. Since the union of a chain of
+  sets is an upper bound for all elements of the chain, the conditions
+  of Zorn's lemma can be modified: if @{text S} is non-empty, it
+  suffices to show that for every non-empty chain @{text c} in @{text
+  S} the union of @{text c} also lies in @{text S}.
+*}
 
-theorem Zorn's_Lemma: 
-  "(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S
-  ==>  EX y: S. ALL z: S. y <= z --> y = z"
+theorem Zorn's_Lemma:
+  "(\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S) \<Longrightarrow> a \<in> S
+  \<Longrightarrow> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z"
 proof (rule Zorn_Lemma2)
   txt_raw {* \footnote{See
   \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *}
-  assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S"
-  assume aS: "a:S"
-  show "ALL c:chain S. EX y:S. ALL z:c. z <= y"
+  assume r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"
+  assume aS: "a \<in> S"
+  show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
   proof
-    fix c assume "c:chain S" 
-    show "EX y:S. ALL z:c. z <= y"
+    fix c assume "c \<in> chain S"
+    show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
     proof cases
  
-      txt{* If $c$ is an empty chain, then every element
-      in $S$ is an upper bound of $c$. *}
+      txt {* If @{text c} is an empty chain, then every element in
+      @{text S} is an upper bound of @{text c}. *}
 
-      assume "c={}" 
+      assume "c = {}" 
       with aS show ?thesis by fast
 
-      txt{* If $c$ is non-empty, then $\Union c$ 
-      is an upper bound of $c$, lying in $S$. *}
+      txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
+      bound of @{text c}, lying in @{text S}. *}
 
     next
-      assume c: "c~={}"
+      assume c: "c \<noteq> {}"
       show ?thesis 
       proof 
-        show "ALL z:c. z <= Union c" by fast
-        show "Union c : S" 
+        show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast
+        show "\<Union>c \<in> S" 
         proof (rule r)
-          from c show "EX x. x:c" by fast  
+          from c show "\<exists>x. x \<in> c" by fast  
         qed
       qed
     qed
   qed
 qed
 
-end
\ No newline at end of file
+end
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/document/bbb.sty
--- a/src/HOL/Real/HahnBanach/document/bbb.sty	Sat Dec 16 21:41:14 2000 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-%
-% home made blackboard-bold symbols: B C D E F G H I J K L M N O P Q R T U Z
-%
-
-\def\bbbB{{{\rm I}\mkern-3.8mu{\rm B}}}
-\def\bbbC{{{\rm C}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
-\def\bbbD{{{\rm I}\mkern-3.8mu{\rm D}}}
-\def\bbbE{{{\rm I}\mkern-3.8mu{\rm E}}}
-\def\bbbF{{{\rm I}\mkern-3.8mu{\rm F}}}
-\def\bbbG{{{\rm G}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbH{{{\rm I}\mkern-3.8mu{\rm H}}}
-\def\bbbI{{{\rm I}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
-\def\bbbJ{{{\rm J}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
-\def\bbbK{{{\rm I}\mkern-3.8mu{\rm K}}}
-\def\bbbL{{{\rm I}\mkern-3.8mu{\rm L}}}
-\def\bbbM{{{\rm I}\mkern-3.8mu{\rm M}}}
-\def\bbbN{{{\rm I}\mkern-3.8mu{\rm N}}}
-\def\bbbO{{{\rm O}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbP{{{\rm I}\mkern-3.8mu{\rm P}}}
-\def\bbbQ{{{\rm Q}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbR{{{\rm I}\mkern-3.8mu{\rm R}}}
-\def\bbbT{{{\rm T}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbU{{{\rm U}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
-\def\bbbZ{{{\sf Z}\mkern-7.5mu{\sf Z}}}
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/document/notation.tex
--- a/src/HOL/Real/HahnBanach/document/notation.tex	Sat Dec 16 21:41:14 2000 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-
-\renewcommand{\isamarkupheader}[1]{\section{#1}}
-\newcommand{\isasymprod}{\isamath{\mult}}
-\newcommand{\isasymzero}{\isamath{\zero}}
-
-\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
-\newcommand{\var}[1]{{?\!#1}}
-\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
-\newcommand{\dsh}{\dshsym}
-
-\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
-
-\newcommand{\skp}{\smallskip}
-
-\newcommand{\To}{\to}
-\newcommand{\dt}{{\mathpunct.}}
-\newcommand{\Ex}[1]{\exists #1\dt\;}
-\newcommand{\Forall}{\forall}
-\newcommand{\All}[1]{\Forall #1\dt\;}
-\newcommand{\Eq}{\mathbin{\,\equiv\,}}
-\newcommand{\Impl}{\Rightarrow}
-\newcommand{\And}{\;\land\;}
-\newcommand{\Or}{\;\lor\;}
-\newcommand{\Le}{\leq}
-\newcommand{\Lt}{\lt}
-\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-%\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
-\newcommand{\ap}{\mathpalette{\mathbin{}}{\mathbin{}}{\mathbin{}}{\mathbin{}}}
-\newcommand{\Union}{\bigcup}
-\newcommand{\Un}{\cup}
-\newcommand{\Int}{\cap}
-
-\newcommand{\norm}[1]{\left\|#1\right\|}
-\newcommand{\fnorm}[1]{\left\|#1\right\|}
-\newcommand{\zero}{0}
-\newcommand{\plus}{\mathbin{\mathbf +}}
-\newcommand{\minus}{\mathbin{\mathbf -}}
-\newcommand{\mult}{\cdot}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/document/root.tex
--- a/src/HOL/Real/HahnBanach/document/root.tex	Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/document/root.tex	Sat Dec 16 21:41:51 2000 +0100
@@ -1,12 +1,16 @@
+
 \documentclass[10pt,a4paper,twoside]{article}
-%\documentclass[11pt,a4paper,twoside]{article}
 
 \usepackage{latexsym,theorem}
-\usepackage{isabelle,isabellesym,bbb}
+\usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup} %last one!
+
+\isabellestyle{it}
 \urlstyle{rm}
 
-\input{notation}
+\newcommand{\isasymsup}{\isamath{\sup\,}}
+\newcommand{\skp}{\smallskip}
+
 
 \begin{document}
 
@@ -50,27 +54,27 @@
 \clearpage
 \part {Basic Notions}
 
-\input{Bounds.tex}
-\input{Aux.tex}
-\input{VectorSpace.tex}
-\input{Subspace.tex}
-\input{NormedSpace.tex}
-\input{Linearform.tex}
-\input{FunctionOrder.tex}
-\input{FunctionNorm.tex}
-\input{ZornLemma.tex}
+\input{Bounds}
+\input{Aux}
+\input{VectorSpace}
+\input{Subspace}
+\input{NormedSpace}
+\input{Linearform}
+\input{FunctionOrder}
+\input{FunctionNorm}
+\input{ZornLemma}
 
 \clearpage
 \part {Lemmas for the Proof}
 
-\input{HahnBanachSupLemmas.tex}
-\input{HahnBanachExtLemmas.tex}
-\input{HahnBanachLemmas.tex}
+\input{HahnBanachSupLemmas}
+\input{HahnBanachExtLemmas}
+\input{HahnBanachLemmas}
 
 \clearpage
 \part {The Main Proof}
 
-\input{HahnBanach.tex}
+\input{HahnBanach}
 \bibliographystyle{abbrv}
 \bibliography{root}