# HG changeset patch
# User ballarin
# Date 1216133409 -7200
# Node ID 2c01c0bdb385303fca5891f3e31933e4cd5b4d0c
# Parent  8882d47e075fa1dd5d22404cb9bea5b2e2f6ac36
Removed uses of context element includes.

diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -60,7 +60,7 @@
   a_r_coset_def r_coset_def
 
 lemma a_r_coset_def':
-  includes struct G
+  fixes G (structure)
   shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}"
 unfolding a_r_coset_defs
 by simp
@@ -69,7 +69,7 @@
   a_l_coset_def l_coset_def
 
 lemma a_l_coset_def':
-  includes struct G
+  fixes G (structure)
   shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}"
 unfolding a_l_coset_defs
 by simp
@@ -78,7 +78,7 @@
   A_RCOSETS_def RCOSETS_def
 
 lemma A_RCOSETS_def':
-  includes struct G
+  fixes G (structure)
   shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}"
 unfolding A_RCOSETS_defs
 by (fold a_r_coset_def, simp)
@@ -87,7 +87,7 @@
   set_add_def set_mult_def
 
 lemma set_add_def':
-  includes struct G
+  fixes G (structure)
   shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"
 unfolding set_add_defs
 by simp
@@ -96,7 +96,7 @@
   A_SET_INV_def SET_INV_def
 
 lemma A_SET_INV_def':
-  includes struct G
+  fixes G (structure)
   shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
 unfolding A_SET_INV_defs
 by (fold a_inv_def)
@@ -188,7 +188,7 @@
 by (rule additive_subgroup_axioms)
 
 lemma additive_subgroupI:
-  includes struct G
+  fixes G (structure)
   assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   shows "additive_subgroup H G"
 by (rule additive_subgroup.intro) (rule a_subgroup)
@@ -240,7 +240,7 @@
 qed
 
 lemma abelian_subgroupI2:
-  includes struct G
+  fixes G (structure)
   assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
       and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   shows "abelian_subgroup H G"
@@ -265,7 +265,7 @@
 qed
 
 lemma abelian_subgroupI3:
-  includes struct G
+  fixes G (structure)
   assumes asg: "additive_subgroup H G"
       and ag: "abelian_group G"
   shows "abelian_subgroup H G"
@@ -451,7 +451,7 @@
 lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
 
 lemma A_FactGroup_def':
-  includes struct G
+  fixes G (structure)
   shows "G A_Mod H \<equiv> \<lparr>carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\<rparr>"
 unfolding A_FactGroup_defs
 by (fold A_RCOSETS_def set_add_def)
@@ -534,16 +534,20 @@
 subsection {* Homomorphisms *}
 
 lemma abelian_group_homI:
-  includes abelian_group G
-  includes abelian_group H
+  assumes "abelian_group G"
+  assumes "abelian_group H"
   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
                                   (| carrier = carrier H, mult = add H, one = zero H |) h"
   shows "abelian_group_hom G H h"
-apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
-  apply (rule G.abelian_group_axioms)
- apply (rule H.abelian_group_axioms)
-apply (rule a_group_hom)
-done
+proof -
+  interpret G: abelian_group [G] by fact
+  interpret H: abelian_group [H] by fact
+  show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
+    apply fact
+    apply fact
+    apply (rule a_group_hom)
+    done
+qed
 
 lemma (in abelian_group_hom) is_abelian_group_hom:
   "abelian_group_hom G H h"
@@ -688,10 +692,11 @@
 
 --"variant"
 lemma (in abelian_subgroup) a_rcos_module_minus:
-  includes ring G
+  assumes "ring G"
   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
 proof -
+  interpret G: ring [G] by fact
   from carr
   have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
   with carr
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/Coset.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -109,23 +109,27 @@
 
 text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
 lemma (in group) repr_independenceD:
-  includes subgroup H G
+  assumes "subgroup H G"
   assumes ycarr: "y \<in> carrier G"
       and repr:  "H #> x = H #> y"
   shows "y \<in> H #> x"
-  apply (subst repr)
+proof -
+  interpret subgroup [H G] by fact
+  show ?thesis  apply (subst repr)
   apply (intro rcos_self)
    apply (rule ycarr)
    apply (rule is_subgroup)
   done
+qed
 
 text {* Elements of a right coset are in the carrier *}
 lemma (in subgroup) elemrcos_carrier:
-  includes group
+  assumes "group G"
   assumes acarr: "a \<in> carrier G"
     and a': "a' \<in> H #> a"
   shows "a' \<in> carrier G"
 proof -
+  interpret group [G] by fact
   from subset and acarr
   have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
   from this and a'
@@ -134,38 +138,42 @@
 qed
 
 lemma (in subgroup) rcos_const:
-  includes group
+  assumes "group G"
   assumes hH: "h \<in> H"
   shows "H #> h = H"
-  apply (unfold r_coset_def)
-  apply rule
-   apply rule
-   apply clarsimp
-   apply (intro subgroup.m_closed)
-     apply (rule is_subgroup)
+proof -
+  interpret group [G] by fact
+  show ?thesis apply (unfold r_coset_def)
+    apply rule
+    apply rule
+    apply clarsimp
+    apply (intro subgroup.m_closed)
+    apply (rule is_subgroup)
     apply assumption
-   apply (rule hH)
-  apply rule
-  apply simp
-proof -
-  fix h'
-  assume h'H: "h' \<in> H"
-  note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
-  from carr
-  have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
-  from h'H hH
-  have "h' \<otimes> inv h \<in> H" by simp
-  from this and a
-  show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
+    apply (rule hH)
+    apply rule
+    apply simp
+  proof -
+    fix h'
+    assume h'H: "h' \<in> H"
+    note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
+    from carr
+    have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
+    from h'H hH
+    have "h' \<otimes> inv h \<in> H" by simp
+    from this and a
+    show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
+  qed
 qed
 
 text {* Step one for lemma @{text "rcos_module"} *}
 lemma (in subgroup) rcos_module_imp:
-  includes group
+  assumes "group G"
   assumes xcarr: "x \<in> carrier G"
       and x'cos: "x' \<in> H #> x"
   shows "(x' \<otimes> inv x) \<in> H"
 proof -
+  interpret group [G] by fact
   from xcarr x'cos
       have x'carr: "x' \<in> carrier G"
       by (rule elemrcos_carrier[OF is_group])
@@ -200,11 +208,12 @@
 
 text {* Step two for lemma @{text "rcos_module"} *}
 lemma (in subgroup) rcos_module_rev:
-  includes group
+  assumes "group G"
   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
       and xixH: "(x' \<otimes> inv x) \<in> H"
   shows "x' \<in> H #> x"
 proof -
+  interpret group [G] by fact
   from xixH
       have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
   from this
@@ -231,27 +240,30 @@
 
 text {* Module property of right cosets *}
 lemma (in subgroup) rcos_module:
-  includes group
+  assumes "group G"
   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
-proof
-  assume "x' \<in> H #> x"
-  from this and carr
-      show "x' \<otimes> inv x \<in> H"
+proof -
+  interpret group [G] by fact
+  show ?thesis proof  assume "x' \<in> H #> x"
+    from this and carr
+    show "x' \<otimes> inv x \<in> H"
       by (intro rcos_module_imp[OF is_group])
-next
-  assume "x' \<otimes> inv x \<in> H"
-  from this and carr
-      show "x' \<in> H #> x"
+  next
+    assume "x' \<otimes> inv x \<in> H"
+    from this and carr
+    show "x' \<in> H #> x"
       by (intro rcos_module_rev[OF is_group])
+  qed
 qed
 
 text {* Right cosets are subsets of the carrier. *} 
 lemma (in subgroup) rcosets_carrier:
-  includes group
+  assumes "group G"
   assumes XH: "X \<in> rcosets H"
   shows "X \<subseteq> carrier G"
 proof -
+  interpret group [G] by fact
   from XH have "\<exists>x\<in> carrier G. X = H #> x"
       unfolding RCOSETS_def
       by fast
@@ -331,11 +343,12 @@
 qed
 
 lemma (in subgroup) lcos_module_rev:
-  includes group
+  assumes "group G"
   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
       and xixH: "(inv x \<otimes> x') \<in> H"
   shows "x' \<in> x <# H"
 proof -
+  interpret group [G] by fact
   from xixH
       have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
   from this
@@ -584,29 +597,33 @@
 
 
 lemma (in subgroup) equiv_rcong:
-   includes group G
+   assumes "group G"
    shows "equiv (carrier G) (rcong H)"
-proof (intro equiv.intro)
-  show "refl (carrier G) (rcong H)"
-    by (auto simp add: r_congruent_def refl_def) 
-next
-  show "sym (rcong H)"
-  proof (simp add: r_congruent_def sym_def, clarify)
-    fix x y
-    assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
-       and "inv x \<otimes> y \<in> H"
-    hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
-    thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
-  qed
-next
-  show "trans (rcong H)"
-  proof (simp add: r_congruent_def trans_def, clarify)
-    fix x y z
-    assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
-       and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
-    hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
-    hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv) 
-    thus "inv x \<otimes> z \<in> H" by simp
+proof -
+  interpret group [G] by fact
+  show ?thesis
+  proof (intro equiv.intro)
+    show "refl (carrier G) (rcong H)"
+      by (auto simp add: r_congruent_def refl_def) 
+  next
+    show "sym (rcong H)"
+    proof (simp add: r_congruent_def sym_def, clarify)
+      fix x y
+      assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
+	 and "inv x \<otimes> y \<in> H"
+      hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
+      thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
+    qed
+  next
+    show "trans (rcong H)"
+    proof (simp add: r_congruent_def trans_def, clarify)
+      fix x y z
+      assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
+	 and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
+      hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
+      hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv) 
+      thus "inv x \<otimes> z \<in> H" by simp
+    qed
   qed
 qed
 
@@ -625,31 +642,38 @@
 *)
 
 lemma (in subgroup) l_coset_eq_rcong:
-  includes group G
+  assumes "group G"
   assumes a: "a \<in> carrier G"
   shows "a <# H = rcong H `` {a}"
-by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
-
+proof -
+  interpret group [G] by fact
+  show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
+qed
 
 subsubsection{*Two Distinct Right Cosets are Disjoint*}
 
 lemma (in group) rcos_equation:
-  includes subgroup H G
-  shows
-     "\<lbrakk>ha \<otimes> a = h \<otimes> b; a \<in> carrier G;  b \<in> carrier G;  
-        h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
-      \<Longrightarrow> hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
-apply (rule UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
-apply (simp add: ) 
-apply (simp add: m_assoc transpose_inv)
-done
+  assumes "subgroup H G"
+  assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
+  shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
+proof -
+  interpret subgroup [H G] by fact
+  from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
+    apply (simp add: )
+    apply (simp add: m_assoc transpose_inv)
+    done
+qed
 
 lemma (in group) rcos_disjoint:
-  includes subgroup H G
-  shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
-apply (simp add: RCOSETS_def r_coset_def)
-apply (blast intro: rcos_equation prems sym)
-done
+  assumes "subgroup H G"
+  assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
+  shows "a \<inter> b = {}"
+proof -
+  interpret subgroup [H G] by fact
+  from p show ?thesis apply (simp add: RCOSETS_def r_coset_def)
+    apply (blast intro: rcos_equation prems sym)
+    done
+qed
 
 subsection {* Further lemmas for @{text "r_congruent"} *}
 
@@ -732,12 +756,16 @@
   "order S \<equiv> card (carrier S)"
 
 lemma (in group) rcosets_part_G:
-  includes subgroup
+  assumes "subgroup H G"
   shows "\<Union>(rcosets H) = carrier G"
-apply (rule equalityI)
- apply (force simp add: RCOSETS_def r_coset_def)
-apply (auto simp add: RCOSETS_def intro: rcos_self prems)
-done
+proof -
+  interpret subgroup [H G] by fact
+  show ?thesis
+    apply (rule equalityI)
+    apply (force simp add: RCOSETS_def r_coset_def)
+    apply (auto simp add: RCOSETS_def intro: rcos_self prems)
+    done
+qed
 
 lemma (in group) cosets_finite:
      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
@@ -815,9 +843,10 @@
 by (auto simp add: RCOSETS_def rcos_sum m_assoc)
 
 lemma (in subgroup) subgroup_in_rcosets:
-  includes group G
+  assumes "group G"
   shows "H \<in> rcosets H"
 proof -
+  interpret group [G] by fact
   from _ subgroup_axioms have "H #> \<one> = H"
     by (rule coset_join2) auto
   then show ?thesis
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -396,9 +396,13 @@
   by (rule subgroup.subset)
 
 lemma (in subgroup) subgroup_is_group [intro]:
-  includes group G
-  shows "group (G\<lparr>carrier := H\<rparr>)" 
-  by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
+  assumes "group G"
+  shows "group (G\<lparr>carrier := H\<rparr>)"
+proof -
+  interpret group [G] by fact
+  show ?thesis
+    by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
+qed
 
 text {*
   Since @{term H} is nonempty, it contains some element @{term x}.  Since
@@ -453,9 +457,11 @@
                 one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
 
 lemma DirProd_monoid:
-  includes monoid G + monoid H
+  assumes "monoid G" and "monoid H"
   shows "monoid (G \<times>\<times> H)"
 proof -
+  interpret G: monoid [G] by fact
+  interpret H: monoid [H] by fact
   from prems
   show ?thesis by (unfold monoid_def DirProd_def, auto) 
 qed
@@ -463,11 +469,15 @@
 
 text{*Does not use the previous result because it's easier just to use auto.*}
 lemma DirProd_group:
-  includes group G + group H
+  assumes "group G" and "group H"
   shows "group (G \<times>\<times> H)"
-  by (rule groupI)
+proof -
+  interpret G: group [G] by fact
+  interpret H: group [H] by fact
+  show ?thesis by (rule groupI)
      (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
            simp add: DirProd_def)
+qed
 
 lemma carrier_DirProd [simp]:
      "carrier (G \<times>\<times> H) = carrier G \<times> carrier H"
@@ -482,23 +492,29 @@
   by (simp add: DirProd_def)
 
 lemma inv_DirProd [simp]:
-  includes group G + group H
+  assumes "group G" and "group H"
   assumes g: "g \<in> carrier G"
       and h: "h \<in> carrier H"
   shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
-  apply (rule group.inv_equality [OF DirProd_group])
+proof -
+  interpret G: group [G] by fact
+  interpret H: group [H] by fact
+  show ?thesis apply (rule group.inv_equality [OF DirProd_group])
   apply (simp_all add: prems group.l_inv)
   done
+qed
 
 text{*This alternative proof of the previous result demonstrates interpret.
    It uses @{text Prod.inv_equality} (available after @{text interpret})
    instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
 lemma
-  includes group G + group H
+  assumes "group G" and "group H"
   assumes g: "g \<in> carrier G"
       and h: "h \<in> carrier H"
   shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
 proof -
+  interpret G: group [G] by fact
+  interpret H: group [H] by fact
   interpret Prod: group ["G \<times>\<times> H"]
     by (auto intro: DirProd_group group.intro group.axioms prems)
   show ?thesis by (simp add: Prod.inv_equality g h)
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -28,18 +28,21 @@
 by (rule ideal_axioms)
 
 lemma idealI:
-  includes ring
+  fixes R (structure)
+  assumes "ring R"
   assumes a_subgroup: "subgroup I \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
       and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
       and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
   shows "ideal I R"
-  apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
+proof -
+  interpret ring [R] by fact
+  show ?thesis  apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
      apply (rule a_subgroup)
     apply (rule is_ring)
    apply (erule (1) I_l_closed)
   apply (erule (1) I_r_closed)
   done
-
+qed
 
 subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
 
@@ -58,11 +61,14 @@
 by (rule principalideal_axioms)
 
 lemma principalidealI:
-  includes ideal
+  fixes R (structure)
+  assumes "ideal I R"
   assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
   shows "principalideal I R"
-  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
-
+proof -
+  interpret ideal [I R] by fact
+  show ?thesis  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
+qed
 
 subsection {* Maximal Ideals *}
 
@@ -75,13 +81,16 @@
 by (rule maximalideal_axioms)
 
 lemma maximalidealI:
-  includes ideal
+  fixes R
+  assumes "ideal I R"
   assumes I_notcarr: "carrier R \<noteq> I"
      and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
   shows "maximalideal I R"
-  by (intro maximalideal.intro maximalideal_axioms.intro)
+proof -
+  interpret ideal [I R] by fact
+  show ?thesis by (intro maximalideal.intro maximalideal_axioms.intro)
     (rule is_ideal, rule I_notcarr, rule I_maximal)
-
+qed
 
 subsection {* Prime Ideals *}
 
@@ -94,31 +103,40 @@
 by (rule primeideal_axioms)
 
 lemma primeidealI:
-  includes ideal
-  includes cring
+  fixes R (structure)
+  assumes "ideal I R"
+  assumes "cring R"
   assumes I_notcarr: "carrier R \<noteq> I"
       and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
   shows "primeideal I R"
-  by (intro primeideal.intro primeideal_axioms.intro)
+proof -
+  interpret ideal [I R] by fact
+  interpret cring [R] by fact
+  show ?thesis by (intro primeideal.intro primeideal_axioms.intro)
     (rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
+qed
 
 lemma primeidealI2:
-  includes additive_subgroup I R
-  includes cring
+  fixes R (structure)
+  assumes "additive_subgroup I R"
+  assumes "cring R"
   assumes I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
       and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
       and I_notcarr: "carrier R \<noteq> I"
       and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
   shows "primeideal I R"
-apply (intro_locales)
- apply (intro ideal_axioms.intro)
-  apply (erule (1) I_l_closed)
- apply (erule (1) I_r_closed)
-apply (intro primeideal_axioms.intro)
- apply (rule I_notcarr)
-apply (erule (2) I_prime)
-done
-
+proof -
+  interpret additive_subgroup [I R] by fact
+  interpret cring [R] by fact
+  show ?thesis apply (intro_locales)
+    apply (intro ideal_axioms.intro)
+    apply (erule (1) I_l_closed)
+    apply (erule (1) I_r_closed)
+    apply (intro primeideal_axioms.intro)
+    apply (rule I_notcarr)
+    apply (erule (2) I_prime)
+    done
+qed
 
 section {* Properties of Ideals *}
 
@@ -185,9 +203,13 @@
 text {* \paragraph{Intersection of two ideals} The intersection of any
   two ideals is again an ideal in @{term R} *}
 lemma (in ring) i_intersect:
-  includes ideal I R
-  includes ideal J R
+  assumes "ideal I R"
+  assumes "ideal J R"
   shows "ideal (I \<inter> J) R"
+proof -
+  interpret ideal [I R] by fact
+  interpret ideal [J R] by fact
+  show ?thesis
 apply (intro idealI subgroup.intro)
       apply (rule is_ring)
      apply (force simp add: a_subset)
@@ -199,7 +221,7 @@
 apply (clarsimp, rule)
  apply (fast intro: ideal.I_r_closed ideal.intro prems)+
 done
-
+qed
 
 subsubsection {* Intersection of a Set of Ideals *}
 
@@ -511,15 +533,18 @@
 text {* @{const "cgenideal"} is minimal *}
 
 lemma (in ring) cgenideal_minimal:
-  includes ideal J R
+  assumes "ideal J R"
   assumes aJ: "a \<in> J"
   shows "PIdl a \<subseteq> J"
-unfolding cgenideal_def
-apply rule
-apply clarify
-using aJ
-apply (erule I_l_closed)
-done
+proof -
+  interpret ideal [J R] by fact
+  show ?thesis unfolding cgenideal_def
+    apply rule
+    apply clarify
+    using aJ
+    apply (erule I_l_closed)
+    done
+qed
 
 lemma (in cring) cgenideal_eq_genideal:
   assumes icarr: "i \<in> carrier R"
@@ -636,9 +661,10 @@
 
 text {* Every principal ideal is a right coset of the carrier *}
 lemma (in principalideal) rcos_generate:
-  includes cring
+  assumes "cring R"
   shows "\<exists>x\<in>I. I = carrier R #> x"
 proof -
+  interpret cring [R] by fact
   from generate
       obtain i
         where icarr: "i \<in> carrier R"
@@ -667,10 +693,11 @@
 subsection {* Prime Ideals *}
 
 lemma (in ideal) primeidealCD:
-  includes cring
+  assumes "cring R"
   assumes notprime: "\<not> primeideal I R"
   shows "carrier R = I \<or> (\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I)"
 proof (rule ccontr, clarsimp)
+  interpret cring [R] by fact
   assume InR: "carrier R \<noteq> I"
      and "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)"
   hence I_prime: "\<And> a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" by simp
@@ -685,11 +712,16 @@
 qed
 
 lemma (in ideal) primeidealCE:
-  includes cring
+  assumes "cring R"
   assumes notprime: "\<not> primeideal I R"
   obtains "carrier R = I"
     | "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
-  using primeidealCD [OF R.is_cring notprime] by blast
+proof -
+  interpret R: cring [R] by fact
+  assume "carrier R = I ==> thesis"
+    and "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I \<Longrightarrow> thesis"
+  then show thesis using primeidealCD [OF R.is_cring notprime] by blast
+qed
 
 text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *}
 lemma (in cring) zeroprimeideal_domainI:
@@ -739,103 +771,108 @@
 qed
 
 lemma (in ideal) helper_max_prime:
-  includes cring
+  assumes "cring R"
   assumes acarr: "a \<in> carrier R"
   shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"
-apply (rule idealI)
-   apply (rule cring.axioms[OF is_cring])
-  apply (rule subgroup.intro)
-     apply (simp, fast)
+proof -
+  interpret cring [R] by fact
+  show ?thesis apply (rule idealI)
+    apply (rule cring.axioms[OF is_cring])
+    apply (rule subgroup.intro)
+    apply (simp, fast)
     apply clarsimp apply (simp add: r_distr acarr)
-   apply (simp add: acarr)
-  apply (simp add: a_inv_def[symmetric], clarify) defer 1
-  apply clarsimp defer 1
-  apply (fast intro!: helper_I_closed acarr)
-proof -
-  fix x
-  assume xcarr: "x \<in> carrier R"
-     and ax: "a \<otimes> x \<in> I"
-  from ax and acarr xcarr
-      have "\<ominus>(a \<otimes> x) \<in> I" by simp
-  also from acarr xcarr
-      have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra
-  finally
-      show "a \<otimes> (\<ominus>x) \<in> I" .
-  from acarr
-      have "a \<otimes> \<zero> = \<zero>" by simp
-next
-  fix x y
-  assume xcarr: "x \<in> carrier R"
-     and ycarr: "y \<in> carrier R"
-     and ayI: "a \<otimes> y \<in> I"
-  from ayI and acarr xcarr ycarr
-      have "a \<otimes> (y \<otimes> x) \<in> I" by (simp add: helper_I_closed)
-  moreover from xcarr ycarr
-      have "y \<otimes> x = x \<otimes> y" by (simp add: m_comm)
-  ultimately
-      show "a \<otimes> (x \<otimes> y) \<in> I" by simp
+    apply (simp add: acarr)
+    apply (simp add: a_inv_def[symmetric], clarify) defer 1
+    apply clarsimp defer 1
+    apply (fast intro!: helper_I_closed acarr)
+  proof -
+    fix x
+    assume xcarr: "x \<in> carrier R"
+      and ax: "a \<otimes> x \<in> I"
+    from ax and acarr xcarr
+    have "\<ominus>(a \<otimes> x) \<in> I" by simp
+    also from acarr xcarr
+    have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra
+    finally
+    show "a \<otimes> (\<ominus>x) \<in> I" .
+    from acarr
+    have "a \<otimes> \<zero> = \<zero>" by simp
+  next
+    fix x y
+    assume xcarr: "x \<in> carrier R"
+      and ycarr: "y \<in> carrier R"
+      and ayI: "a \<otimes> y \<in> I"
+    from ayI and acarr xcarr ycarr
+    have "a \<otimes> (y \<otimes> x) \<in> I" by (simp add: helper_I_closed)
+    moreover from xcarr ycarr
+    have "y \<otimes> x = x \<otimes> y" by (simp add: m_comm)
+    ultimately
+    show "a \<otimes> (x \<otimes> y) \<in> I" by simp
+  qed
 qed
 
 text {* In a cring every maximal ideal is prime *}
 lemma (in cring) maximalideal_is_prime:
-  includes maximalideal
+  assumes "maximalideal I R"
   shows "primeideal I R"
-apply (rule ccontr)
-apply (rule primeidealCE)
-   apply (rule is_cring)
-  apply assumption
- apply (simp add: I_notcarr)
 proof -
-  assume "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
-  from this
-      obtain a b
-        where acarr: "a \<in> carrier R"
-        and bcarr: "b \<in> carrier R"
-        and abI: "a \<otimes> b \<in> I"
-        and anI: "a \<notin> I"
-        and bnI: "b \<notin> I"
+  interpret maximalideal [I R] by fact
+  show ?thesis apply (rule ccontr)
+    apply (rule primeidealCE)
+    apply (rule is_cring)
+    apply assumption
+    apply (simp add: I_notcarr)
+  proof -
+    assume "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
+    from this
+    obtain a b
+      where acarr: "a \<in> carrier R"
+      and bcarr: "b \<in> carrier R"
+      and abI: "a \<otimes> b \<in> I"
+      and anI: "a \<notin> I"
+      and bnI: "b \<notin> I"
       by fast
-  def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
-
-  from R.is_cring and acarr
-  have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
-
-  have IsubJ: "I \<subseteq> J"
-  proof
-    fix x
-    assume xI: "x \<in> I"
-    from this and acarr
-    have "a \<otimes> x \<in> I" by (intro I_l_closed)
-    from xI[THEN a_Hcarr] this
-    show "x \<in> J" unfolding J_def by fast
+    def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
+    
+    from R.is_cring and acarr
+    have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
+    
+    have IsubJ: "I \<subseteq> J"
+    proof
+      fix x
+      assume xI: "x \<in> I"
+      from this and acarr
+      have "a \<otimes> x \<in> I" by (intro I_l_closed)
+      from xI[THEN a_Hcarr] this
+      show "x \<in> J" unfolding J_def by fast
+    qed
+    
+    from abI and acarr bcarr
+    have "b \<in> J" unfolding J_def by fast
+    from bnI and this
+    have JnI: "J \<noteq> I" by fast
+    from acarr
+    have "a = a \<otimes> \<one>" by algebra
+    from this and anI
+    have "a \<otimes> \<one> \<notin> I" by simp
+    from one_closed and this
+    have "\<one> \<notin> J" unfolding J_def by fast
+    hence Jncarr: "J \<noteq> carrier R" by fast
+    
+    interpret ideal ["J" "R"] by (rule idealJ)
+    
+    have "J = I \<or> J = carrier R"
+      apply (intro I_maximal)
+      apply (rule idealJ)
+      apply (rule IsubJ)
+      apply (rule a_subset)
+      done
+    
+    from this and JnI and Jncarr
+    show "False" by simp
   qed
-
-  from abI and acarr bcarr
-      have "b \<in> J" unfolding J_def by fast
-  from bnI and this
-      have JnI: "J \<noteq> I" by fast
-  from acarr
-      have "a = a \<otimes> \<one>" by algebra
-  from this and anI
-      have "a \<otimes> \<one> \<notin> I" by simp
-  from one_closed and this
-      have "\<one> \<notin> J" unfolding J_def by fast
-  hence Jncarr: "J \<noteq> carrier R" by fast
-
-  interpret ideal ["J" "R"] by (rule idealJ)
-
-  have "J = I \<or> J = carrier R"
-     apply (intro I_maximal)
-     apply (rule idealJ)
-     apply (rule IsubJ)
-     apply (rule a_subset)
-     done
-
-  from this and JnI and Jncarr
-      show "False" by simp
 qed
 
-
 subsection {* Derived Theorems Involving Ideals *}
 
 --"A non-zero cring that has only the two trivial ideals is a field"
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -155,27 +155,32 @@
 
 text {* The quotient of a cring is also commutative *}
 lemma (in ideal) quotient_is_cring:
-  includes cring
+  assumes "cring R"
   shows "cring (R Quot I)"
-apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
+proof -
+  interpret cring [R] by fact
+  show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
   apply (rule quotient_is_ring)
  apply (rule ring.axioms[OF quotient_is_ring])
 apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric])
 apply clarify
 apply (simp add: rcoset_mult_add m_comm)
 done
+qed
 
 text {* Cosets as a ring homomorphism on crings *}
 lemma (in ideal) rcos_ring_hom_cring:
-  includes cring
+  assumes "cring R"
   shows "ring_hom_cring R (R Quot I) (op +> I)"
-apply (rule ring_hom_cringI)
+proof -
+  interpret cring [R] by fact
+  show ?thesis apply (rule ring_hom_cringI)
   apply (rule rcos_ring_hom_ring)
  apply (rule R.is_cring)
 apply (rule quotient_is_cring)
 apply (rule R.is_cring)
 done
-
+qed
 
 subsection {* Factorization over Prime Ideals *}
 
@@ -236,9 +241,11 @@
         The proof follows ``W. Adkins, S. Weintraub: Algebra --
         An Approach via Module Theory'' *}
 lemma (in maximalideal) quotient_is_field:
-  includes cring
+  assumes "cring R"
   shows "field (R Quot I)"
-apply (intro cring.cring_fieldI2)
+proof -
+  interpret cring [R] by fact
+  show ?thesis apply (intro cring.cring_fieldI2)
   apply (rule quotient_is_cring, rule is_cring)
  defer 1
  apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
@@ -338,5 +345,6 @@
   from rcarr and this[symmetric]
   show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
 qed
+qed
 
 end
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/Ring.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -539,16 +539,26 @@
 text {* Two examples for use of method algebra *}
 
 lemma
-  includes ring R + cring S
-  shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==> 
-  a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
-  by algebra
+  fixes R (structure) and S (structure)
+  assumes "ring R" "cring S"
+  assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
+  shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
+proof -
+  interpret ring [R] by fact
+  interpret cring [S] by fact
+ML_val {* Algebra.print_structures @{context} *}
+  from RS show ?thesis by algebra
+qed
 
 lemma
-  includes cring
-  shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
-  by algebra
-
+  fixes R (structure)
+  assumes "ring R"
+  assumes R: "a \<in> carrier R" "b \<in> carrier R"
+  shows "a \<ominus> (a \<ominus> b) = b"
+proof -
+  interpret ring [R] by fact
+  from R show ?thesis by algebra
+qed
 
 subsubsection {* Sums over Finite Sets *}
 
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -31,55 +31,73 @@
 done
 
 lemma (in ring_hom_ring) is_ring_hom_ring:
-  includes struct R + struct S
-  shows "ring_hom_ring R S h"
-by (rule ring_hom_ring_axioms)
+  "ring_hom_ring R S h"
+  by (rule ring_hom_ring_axioms)
 
 lemma ring_hom_ringI:
-  includes ring R + ring S
+  fixes R (structure) and S (structure)
+  assumes "ring R" "ring S"
   assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
           hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
       and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
       and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
   shows "ring_hom_ring R S h"
-apply unfold_locales
+proof -
+  interpret ring [R] by fact
+  interpret ring [S] by fact
+  show ?thesis apply unfold_locales
 apply (unfold ring_hom_def, safe)
    apply (simp add: hom_closed Pi_def)
   apply (erule (1) compatible_mult)
  apply (erule (1) compatible_add)
 apply (rule compatible_one)
 done
+qed
 
 lemma ring_hom_ringI2:
-  includes ring R + ring S
+  assumes "ring R" "ring S"
   assumes h: "h \<in> ring_hom R S"
   shows "ring_hom_ring R S h"
-apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
-apply (rule R.is_ring)
-apply (rule S.is_ring)
-apply (rule h)
-done
+proof -
+  interpret R: ring [R] by fact
+  interpret S: ring [S] by fact
+  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
+    apply (rule R.is_ring)
+    apply (rule S.is_ring)
+    apply (rule h)
+    done
+qed
 
 lemma ring_hom_ringI3:
-  includes abelian_group_hom R S + ring R + ring S 
+  fixes R (structure) and S (structure)
+  assumes "abelian_group_hom R S h" "ring R" "ring S" 
   assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
       and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
   shows "ring_hom_ring R S h"
-apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
-apply (insert group_hom.homh[OF a_group_hom])
-apply (unfold hom_def ring_hom_def, simp)
-apply safe
-apply (erule (1) compatible_mult)
-apply (rule compatible_one)
-done
+proof -
+  interpret abelian_group_hom [R S h] by fact
+  interpret R: ring [R] by fact
+  interpret S: ring [S] by fact
+  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
+    apply (insert group_hom.homh[OF a_group_hom])
+    apply (unfold hom_def ring_hom_def, simp)
+    apply safe
+    apply (erule (1) compatible_mult)
+    apply (rule compatible_one)
+    done
+qed
 
 lemma ring_hom_cringI:
-  includes ring_hom_ring R S h + cring R + cring S
+  assumes "ring_hom_ring R S h" "cring R" "cring S"
   shows "ring_hom_cring R S h"
-  by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
+proof -
+  interpret ring_hom_ring [R S h] by fact
+  interpret R: cring [R] by fact
+  interpret S: cring [S] by fact
+  show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
     (rule R.is_cring, rule S.is_cring, rule homh)
-
+qed
 
 subsection {* The kernel of a ring homomorphism *}
 
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -1254,15 +1254,17 @@
     cring.axioms prems)
 
 lemma (in UP_pre_univ_prop) UP_hom_unique:
-  includes ring_hom_cring P S Phi
+  assumes "ring_hom_cring P S Phi"
   assumes Phi: "Phi (monom P \<one> (Suc 0)) = s"
       "!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
-  includes ring_hom_cring P S Psi
+  assumes "ring_hom_cring P S Psi"
   assumes Psi: "Psi (monom P \<one> (Suc 0)) = s"
       "!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
     and P: "p \<in> carrier P" and S: "s \<in> carrier S"
   shows "Phi p = Psi p"
 proof -
+  interpret ring_hom_cring [P S Phi] by fact
+  interpret ring_hom_cring [P S Psi] by fact
   have "Phi p =
       Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
     by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -753,11 +753,14 @@
 *}
 
 lemma fold_fusion:
-  includes ab_semigroup_mult g
+  assumes "ab_semigroup_mult g"
   assumes fin: "finite A"
     and hyp: "\<And>x y. h (g x y) = times x (h y)"
   shows "h (fold g j w A) = fold times j (h w) A"
-  using fin hyp by (induct set: finite) simp_all
+proof -
+  interpret ab_semigroup_mult [g] by fact
+  show ?thesis using fin hyp by (induct set: finite) simp_all
+qed
 
 lemma fold_cong:
   "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold times g z A = fold times h z A"
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Hyperreal/FrechetDeriv.thy
--- a/src/HOL/Hyperreal/FrechetDeriv.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Hyperreal/FrechetDeriv.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -61,19 +61,23 @@
 by simp
 
 lemma bounded_linear_add:
-  includes bounded_linear f
-  includes bounded_linear g
+  assumes "bounded_linear f"
+  assumes "bounded_linear g"
   shows "bounded_linear (\<lambda>x. f x + g x)"
-apply (unfold_locales)
-apply (simp only: f.add g.add add_ac)
-apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
-apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
-apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
-apply (rule_tac x="Kf + Kg" in exI, safe)
-apply (subst right_distrib)
-apply (rule order_trans [OF norm_triangle_ineq])
-apply (rule add_mono, erule spec, erule spec)
-done
+proof -
+  interpret f: bounded_linear [f] by fact
+  interpret g: bounded_linear [g] by fact
+  show ?thesis apply (unfold_locales)
+    apply (simp only: f.add g.add add_ac)
+    apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
+    apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
+    apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
+    apply (rule_tac x="Kf + Kg" in exI, safe)
+    apply (subst right_distrib)
+    apply (rule order_trans [OF norm_triangle_ineq])
+    apply (rule add_mono, erule spec, erule spec)
+    done
+qed
 
 lemma norm_ratio_ineq:
   fixes x y :: "'a::real_normed_vector"
@@ -117,13 +121,16 @@
 subsection {* Subtraction *}
 
 lemma bounded_linear_minus:
-  includes bounded_linear f
+  assumes "bounded_linear f"
   shows "bounded_linear (\<lambda>x. - f x)"
-apply (unfold_locales)
-apply (simp add: f.add)
-apply (simp add: f.scaleR)
-apply (simp add: f.bounded)
-done
+proof -
+  interpret f: bounded_linear [f] by fact
+  show ?thesis apply (unfold_locales)
+    apply (simp add: f.add)
+    apply (simp add: f.scaleR)
+    apply (simp add: f.bounded)
+    done
+qed
 
 lemma FDERIV_minus:
   "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)"
@@ -169,30 +176,34 @@
 by simp
 
 lemma bounded_linear_compose:
-  includes bounded_linear f
-  includes bounded_linear g
+  assumes "bounded_linear f"
+  assumes "bounded_linear g"
   shows "bounded_linear (\<lambda>x. f (g x))"
-proof (unfold_locales)
-  fix x y show "f (g (x + y)) = f (g x) + f (g y)"
-    by (simp only: f.add g.add)
-next
-  fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
-    by (simp only: f.scaleR g.scaleR)
-next
-  from f.pos_bounded
-  obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
-  from g.pos_bounded
-  obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
-  show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
-  proof (intro exI allI)
-    fix x
-    have "norm (f (g x)) \<le> norm (g x) * Kf"
-      using f .
-    also have "\<dots> \<le> (norm x * Kg) * Kf"
-      using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
-    also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
-      by (rule mult_assoc)
-    finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
+proof -
+  interpret f: bounded_linear [f] by fact
+  interpret g: bounded_linear [g] by fact
+  show ?thesis proof (unfold_locales)
+    fix x y show "f (g (x + y)) = f (g x) + f (g y)"
+      by (simp only: f.add g.add)
+  next
+    fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
+      by (simp only: f.scaleR g.scaleR)
+  next
+    from f.pos_bounded
+    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
+    from g.pos_bounded
+    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
+    show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
+    proof (intro exI allI)
+      fix x
+      have "norm (f (g x)) \<le> norm (g x) * Kf"
+	using f .
+      also have "\<dots> \<le> (norm x * Kg) * Kf"
+	using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
+      also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
+	by (rule mult_assoc)
+      finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
+    qed
   qed
 qed
 
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -1421,9 +1421,12 @@
 qed
 
 lemma fold_mset_fusion:
-  includes left_commutative g
-  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A"
-by (induct A) auto
+  assumes "left_commutative g"
+  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
+proof -
+  interpret left_commutative [g] by fact
+  show "PROP ?P" by (induct A) auto
+qed
 
 lemma fold_mset_rec:
   assumes "a \<in># A" 
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/MicroJava/BV/Err.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -135,19 +135,21 @@
   "~(Err <_(le r) x)"
   by (simp add: lesssub_def lesub_def le_def split: err.split)
 
-lemma semilat_errI [intro]: includes semilat
-shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
-apply(insert semilat)
-apply (unfold semilat_Def closed_def plussub_def lesub_def 
-              lift2_def Err.le_def err_def)
-apply (simp split: err.split)
-done
+lemma semilat_errI [intro]:
+  assumes semilat: "semilat (A, r, f)"
+  shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
+  apply(insert semilat)
+  apply (unfold semilat_Def closed_def plussub_def lesub_def 
+    lift2_def Err.le_def err_def)
+  apply (simp split: err.split)
+  done
 
 lemma err_semilat_eslI_aux:
-includes semilat shows "err_semilat(esl(A,r,f))"
-apply (unfold sl_def esl_def)
-apply (simp add: semilat_errI[OF semilat])
-done
+  assumes semilat: "semilat (A, r, f)"
+  shows "err_semilat(esl(A,r,f))"
+  apply (unfold sl_def esl_def)
+  apply (simp add: semilat_errI[OF semilat])
+  done
 
 lemma err_semilat_eslI [intro, simp]:
  "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -313,36 +313,44 @@
   apply (blast intro: order_trans)
   done
 
-lemma termination_lemma: includes semilat
-shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
-      ss <[r] merges f qs ss \<or> 
-  merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w"
-apply(insert semilat)
-  apply (unfold lesssub_def)
-  apply (simp (no_asm_simp) add: merges_incr)
-  apply (rule impI)
-  apply (rule merges_same_conv [THEN iffD1, elim_format]) 
-  apply assumption+
+lemma termination_lemma:
+  assumes semilat: "semilat (A, r, f)"
+  shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
+  ss <[r] merges f qs ss \<or> 
+  merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w" (is "PROP ?P")
+proof -
+  interpret semilat [A r f] by fact
+  show "PROP ?P" apply(insert semilat)
+    apply (unfold lesssub_def)
+    apply (simp (no_asm_simp) add: merges_incr)
+    apply (rule impI)
+    apply (rule merges_same_conv [THEN iffD1, elim_format]) 
+    apply assumption+
     defer
     apply (rule sym, assumption)
-   defer apply simp
-   apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
-   apply (blast intro!: psubsetI elim: equalityE)
-   apply clarsimp
-   apply (drule bspec, assumption) 
-   apply (drule bspec, assumption)
-   apply clarsimp
-  done 
+    defer apply simp
+    apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
+    apply (blast intro!: psubsetI elim: equalityE)
+    apply clarsimp
+    apply (drule bspec, assumption) 
+    apply (drule bspec, assumption)
+    apply clarsimp
+    done
+qed
 
-lemma iter_properties[rule_format]: includes semilat
-shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
+lemma iter_properties[rule_format]:
+  assumes semilat: "semilat (A, r, f)"
+  shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
      bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
      \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
    iter f step ss0 w0 = (ss',w')
    \<longrightarrow>
    ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and>
    (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
-apply(insert semilat)
+  (is "PROP ?P")
+proof -
+  interpret semilat [A r f] by fact
+  show "PROP ?P" apply(insert semilat)
 apply (unfold iter_def stables_def)
 apply (rule_tac P = "%(ss,w).
  ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
@@ -434,8 +442,10 @@
 apply clarsimp
 done
 
+qed
 
-lemma kildall_properties: includes semilat
+lemma kildall_properties:
+assumes semilat: "semilat (A, r, f)"
 shows "\<lbrakk> acc r; pres_type step n A; mono r step n A;
      bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
   kildall r f step ss0 \<in> list n A \<and>
@@ -443,6 +453,10 @@
   ss0 <=[r] kildall r f step ss0 \<and>
   (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow>
                  kildall r f step ss0 <=[r] ts)"
+  (is "PROP ?P")
+proof -
+  interpret semilat [A r f] by fact
+  show "PROP ?P"
 apply (unfold kildall_def)
 apply(case_tac "iter f step ss0 (unstables r step ss0)")
 apply(simp)
@@ -450,11 +464,16 @@
 apply (simp_all add: unstables_def stable_def)
 apply (rule semilat)
 done
-
+qed
 
-lemma is_bcv_kildall: includes semilat
+lemma is_bcv_kildall:
+assumes semilat: "semilat (A, r, f)"
 shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk>
   \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
+  (is "PROP ?P")
+proof -
+  interpret semilat [A r f] by fact
+  show "PROP ?P"
 apply(unfold is_bcv_def wt_step_def)
 apply(insert semilat kildall_properties[of A])
 apply(simp add:stables_def)
@@ -472,5 +491,6 @@
  apply simp
 apply (blast intro!: le_listD less_lengthI)
 done
+qed
 
 end
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -378,7 +378,10 @@
 
 
 lemma Listn_sl_aux:
-includes semilat shows "semilat (Listn.sl n (A,r,f))"
+assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))"
+proof -
+  interpret semilat [A r f] by fact
+show ?thesis
 apply (unfold Listn.sl_def)
 apply (simp (no_asm) only: semilat_Def split_conv)
 apply (rule conjI)
@@ -388,6 +391,7 @@
 apply (simp (no_asm) only: list_def)
 apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
 done
+qed
 
 lemma Listn_sl: "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
  by(simp add: Listn_sl_aux split_tupled_all)
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/MicroJava/BV/SemilatAlg.thy
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -62,17 +62,20 @@
   done
 
 
-lemma plusplus_closed: includes semilat shows
-  "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
-proof (induct x)
-  show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
-  fix y x xs
-  assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
-  assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
-  from xs obtain x: "x \<in> A" and xs': "set xs \<subseteq> A" by simp
-  from x y have "(x +_f y) \<in> A" ..
-  with xs' have "xs ++_f (x +_f y) \<in> A" by (rule IH)
-  thus "(x#xs) ++_f y \<in> A" by simp
+lemma plusplus_closed: assumes "semilat (A, r, f)" shows
+  "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A" (is "PROP ?P")
+proof -
+  interpret semilat [A r f] by fact
+  show "PROP ?P" proof (induct x)
+    show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
+    fix y x xs
+    assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
+    assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
+    from xs obtain x: "x \<in> A" and xs': "set xs \<subseteq> A" by simp
+    from x y have "(x +_f y) \<in> A" ..
+    with xs' have "xs ++_f (x +_f y) \<in> A" by (rule IH)
+    thus "(x#xs) ++_f y \<in> A" by simp
+  qed
 qed
 
 lemma (in semilat) pp_ub2:
@@ -154,10 +157,13 @@
 qed
 
 
-lemma ub1': includes semilat
-shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> 
+lemma ub1':
+  assumes "semilat (A, r, f)"
+  shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> 
   \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y" 
 proof -
+  interpret semilat [A r f] by fact
+
   let "b <=_r ?map ++_f y" = ?thesis
 
   assume "y \<in> A"
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -24,23 +24,26 @@
   the_lub  ("\<Squnion>_" [90] 90)
 
 lemma the_lub_equality [elim?]:
-  includes lub
+  assumes "lub A x"
   shows "\<Squnion>A = (x::'a::order)"
-proof (unfold the_lub_def)
-  from lub_axioms show "The (lub A) = x"
-  proof
-    fix x' assume lub': "lub A x'"
-    show "x' = x"
-    proof (rule order_antisym)
-      from lub' show "x' \<le> x"
-      proof
-        fix a assume "a \<in> A"
-        then show "a \<le> x" ..
-      qed
-      show "x \<le> x'"
-      proof
-        fix a assume "a \<in> A"
-        with lub' show "a \<le> x'" ..
+proof -
+  interpret lub [A x] by fact
+  show ?thesis proof (unfold the_lub_def)
+    from `lub A x` show "The (lub A) = x"
+    proof
+      fix x' assume lub': "lub A x'"
+      show "x' = x"
+      proof (rule order_antisym)
+	from lub' show "x' \<le> x"
+	proof
+          fix a assume "a \<in> A"
+          then show "a \<le> x" ..
+	qed
+	show "x \<le> x'"
+	proof
+          fix a assume "a \<in> A"
+          with lub' show "a \<le> x'" ..
+	qed
       qed
     qed
   qed
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -26,7 +26,8 @@
 declare continuous.intro [intro?] continuous_axioms.intro [intro?]
 
 lemma continuousI [intro]:
-  includes norm_syntax + linearform
+  fixes norm :: "_ \<Rightarrow> real"  ("\<parallel>_\<parallel>")
+  assumes "linearform V f"
   assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
   shows "continuous V norm f"
 proof
@@ -74,6 +75,8 @@
   fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
   defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
 
+locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm
+
 lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
   by (simp add: B_def)
 
@@ -82,20 +85,11 @@
   normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
 *}
 
-(* Alternative statement of the lemma as
-     lemma (in fn_norm)
-       includes normed_vectorspace + continuous
-       shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-   is not possible:
-   fn_norm contrains parameter norm to type "'a::zero => real",
-   normed_vectorspace and continuous contrain this parameter to
-   "'a::{minus, plus, zero} => real, which is less general.
-*)
-
-lemma (in normed_vectorspace) fn_norm_works:
-  includes fn_norm + continuous
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
+  assumes "continuous V norm f"
   shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
 proof -
+  interpret continuous [V norm f] by fact
   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 supremum. *}
@@ -158,39 +152,40 @@
   then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex)
 qed
 
-lemma (in normed_vectorspace) fn_norm_ub [iff?]:
-  includes fn_norm + continuous
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
+  assumes "continuous V norm f"
   assumes b: "b \<in> B V f"
   shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
+  interpret continuous [V norm f] by fact
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    unfolding B_def fn_norm_def
     using `continuous V norm f` by (rule fn_norm_works)
   from this and b show ?thesis ..
 qed
 
-lemma (in normed_vectorspace) fn_norm_leastB:
-  includes fn_norm + continuous
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
+  assumes "continuous V norm f"
   assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
 proof -
+  interpret continuous [V norm f] by fact
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    unfolding B_def fn_norm_def
     using `continuous V norm f` by (rule fn_norm_works)
   from this and b show ?thesis ..
 qed
 
 text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
 
-lemma (in normed_vectorspace) fn_norm_ge_zero [iff]:
-  includes fn_norm + continuous
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
+  assumes "continuous V norm f"
   shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
+  interpret continuous [V norm f] by fact
   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. *}
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    unfolding B_def fn_norm_def
+(*    unfolding B_def fn_norm_def *)
     using `continuous V norm f` by (rule fn_norm_works)
   moreover have "0 \<in> B V f" ..
   ultimately show ?thesis ..
@@ -203,34 +198,37 @@
   \end{center}
 *}
 
-lemma (in normed_vectorspace) fn_norm_le_cong:
-  includes fn_norm + continuous + linearform
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
+  assumes "continuous V norm f" "linearform V f"
   assumes x: "x \<in> V"
   shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
-proof cases
-  assume "x = 0"
-  then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
-  also have "f 0 = 0" by rule unfold_locales
-  also have "\<bar>\<dots>\<bar> = 0" by simp
-  also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
-    unfolding B_def fn_norm_def
-    using `continuous V norm f` by (rule fn_norm_ge_zero)
-  from x have "0 \<le> norm x" ..
-  with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
-  finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
-next
-  assume "x \<noteq> 0"
-  with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
-  then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
-  also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
-  proof (rule mult_right_mono)
-    from x show "0 \<le> \<parallel>x\<parallel>" ..
-    from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
-      by (auto simp add: B_def real_divide_def)
-    with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
-      unfolding B_def fn_norm_def by (rule fn_norm_ub)
+proof -
+  interpret continuous [V norm f] by fact
+  interpret linearform [V f] .
+  show ?thesis proof cases
+    assume "x = 0"
+    then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
+    also have "f 0 = 0" by rule unfold_locales
+    also have "\<bar>\<dots>\<bar> = 0" by simp
+    also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
+      using `continuous V norm f` by (rule fn_norm_ge_zero)
+    from x have "0 \<le> norm x" ..
+    with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
+    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
+  next
+    assume "x \<noteq> 0"
+    with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
+    then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
+    also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
+    proof (rule mult_right_mono)
+      from x show "0 \<le> \<parallel>x\<parallel>" ..
+      from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
+	by (auto simp add: B_def real_divide_def)
+      with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
+	by (rule fn_norm_ub)
+    qed
+    finally show ?thesis .
   qed
-  finally show ?thesis .
 qed
 
 text {*
@@ -241,35 +239,38 @@
   \end{center}
 *}
 
-lemma (in normed_vectorspace) fn_norm_least [intro?]:
-  includes fn_norm + continuous
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
+  assumes "continuous V norm f"
   assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
-proof (rule fn_norm_leastB [folded B_def fn_norm_def])
-  fix b assume b: "b \<in> B V f"
-  show "b \<le> c"
-  proof cases
-    assume "b = 0"
-    with ge show ?thesis by simp
-  next
-    assume "b \<noteq> 0"
-    with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
+proof -
+  interpret continuous [V norm f] by fact
+  show ?thesis proof (rule fn_norm_leastB [folded B_def fn_norm_def])
+    fix b assume b: "b \<in> B V f"
+    show "b \<le> c"
+    proof cases
+      assume "b = 0"
+      with ge show ?thesis by simp
+    next
+      assume "b \<noteq> 0"
+      with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
         and x_neq: "x \<noteq> 0" and x: "x \<in> V"
-      by (auto simp add: B_def real_divide_def)
-    note b_rep
-    also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
-    proof (rule mult_right_mono)
-      have "0 < \<parallel>x\<parallel>" using x x_neq ..
-      then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
-      from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+	by (auto simp add: B_def real_divide_def)
+      note b_rep
+      also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
+      proof (rule mult_right_mono)
+	have "0 < \<parallel>x\<parallel>" using x x_neq ..
+	then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
+	from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+      qed
+      also have "\<dots> = c"
+      proof -
+	from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
+	then show ?thesis by simp
+      qed
+      finally show ?thesis .
     qed
-    also have "\<dots> = c"
-    proof -
-      from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
-      then show ?thesis by simp
-    qed
-    finally show ?thesis .
-  qed
-qed (insert `continuous V norm f`, simp_all add: continuous_def)
+  qed (insert `continuous V norm f`, simp_all add: continuous_def)
+qed
 
 end
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -53,17 +53,21 @@
 *}
 
 theorem HahnBanach:
-  includes vectorspace E + subspace F E + seminorm E p + linearform F f
+  assumes E: "vectorspace E" and "subspace F E"
+    and "seminorm E p" and "linearform F f"
   assumes fp: "\<forall>x \<in> F. f x \<le> p x"
   shows "\<exists>h. 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 -
+  interpret vectorspace [E] by fact
+  interpret subspace [F E] by fact
+  interpret seminorm [E p] by fact
+  interpret linearform [F f] by fact
   def M \<equiv> "norm_pres_extensions E p F f"
   hence M: "M = \<dots>" by (simp only:)
-  note E = `vectorspace E`
-  then have F: "vectorspace F" ..
+  from E have F: "vectorspace F" ..
   note FE = `F \<unlhd> E`
   {
     fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c"
@@ -306,17 +310,22 @@
 *}
 
 theorem abs_HahnBanach:
-  includes vectorspace E + subspace F E + linearform F f + seminorm E p
+  assumes E: "vectorspace E" and FE: "subspace F E"
+    and lf: "linearform F f" and sn: "seminorm E p"
   assumes fp: "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
   shows "\<exists>g. 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 -
-  note E = `vectorspace E`
+  interpret vectorspace [E] by fact
+  interpret subspace [F E] by fact
+  interpret linearform [F f] by fact
+  interpret seminorm [E p] by fact
+(*  note E = `vectorspace E`
   note FE = `subspace F E`
   note sn = `seminorm E p`
   note lf = `linearform F f`
-  have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
+*)  have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
   using E FE sn lf
   proof (rule HahnBanach)
     show "\<forall>x \<in> F. f x \<le> p x"
@@ -342,22 +351,31 @@
 *}
 
 theorem norm_HahnBanach:
-  includes normed_vectorspace E + subspace F E + linearform F f + fn_norm + continuous F norm ("\<parallel>_\<parallel>") f
+  fixes V and norm ("\<parallel>_\<parallel>")
+  fixes B defines "\<And>V f. B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
+  fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
+  defines "\<And>V f. \<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
+  assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
+    and linearform: "linearform F f" and "continuous F norm f"
   shows "\<exists>g. linearform E g
      \<and> continuous E norm g
      \<and> (\<forall>x \<in> F. g x = f x)
      \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
 proof -
+  interpret normed_vectorspace [E norm] by fact
+  interpret normed_vectorspace_with_fn_norm [E norm B fn_norm]
+    by (auto simp: B_def fn_norm_def) intro_locales
+  interpret subspace [F E] by fact
+  interpret linearform [F f] by fact
+  interpret continuous [F norm f] by fact
   have E: "vectorspace E" by unfold_locales
-  have E_norm: "normed_vectorspace E norm" by rule unfold_locales
-  note FE = `F \<unlhd> E`
   have F: "vectorspace F" by rule unfold_locales
-  note linearform = `linearform F f`
   have F_norm: "normed_vectorspace F norm"
     using FE E_norm by (rule subspace_normed_vs)
   have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
-    by (rule normed_vectorspace.fn_norm_ge_zero
-      [OF F_norm `continuous F norm f`, folded B_def fn_norm_def])
+    by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
+      [OF normed_vectorspace_with_fn_norm.intro,
+       OF F_norm `continuous F norm f` , folded B_def fn_norm_def])
   txt {* We define a function @{text p} on @{text E} as follows:
     @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
   def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
@@ -406,8 +424,9 @@
     fix x assume "x \<in> F"
     from this and `continuous F norm f`
     show "\<bar>f x\<bar> \<le> p x"
-      by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
-        [OF F_norm, folded B_def fn_norm_def])
+      by (unfold p_def) (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
+        [OF normed_vectorspace_with_fn_norm.intro,
+         OF F_norm, folded B_def fn_norm_def])
   qed
 
   txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
@@ -463,7 +482,9 @@
     txt {* The other direction is achieved by a similar argument. *}
 
     show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
-    proof (rule normed_vectorspace.fn_norm_least [OF F_norm, folded B_def fn_norm_def])
+    proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
+	[OF normed_vectorspace_with_fn_norm.intro,
+	 OF F_norm, folded B_def fn_norm_def])
       show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
       proof
 	fix x assume x: "x \<in> F"
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -40,10 +40,11 @@
 *}
 
 lemma ex_xi:
-  includes vectorspace F
+  assumes "vectorspace F"
   assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
   shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
 proof -
+  interpret vectorspace [F] by fact
   txt {* From the completeness of the reals follows:
     The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
     non-empty and has an upper bound. *}
@@ -86,183 +87,190 @@
 *}
 
 lemma h'_lf:
-  includes var H + var h + var E
   assumes 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' \<equiv> H + lin x0"
     and HE: "H \<unlhd> E"
-  includes linearform H h
+  assumes "linearform H h"
   assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
-  includes vectorspace E
+  assumes E: "vectorspace E"
   shows "linearform H' h'"
-proof
-  note E = `vectorspace E`
-  have H': "vectorspace H'"
-  proof (unfold H'_def)
-    from `x0 \<in> E`
-    have "lin x0 \<unlhd> E" ..
-    with HE show "vectorspace (H + lin x0)" using E ..
-  qed
-  {
-    fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
-    show "h' (x1 + x2) = h' x1 + h' x2"
-    proof -
-      from H' x1 x2 have "x1 + x2 \<in> H'"
-        by (rule vectorspace.add_closed)
-      with x1 x2 obtain y y1 y2 a a1 a2 where
-            x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
+proof -
+  interpret linearform [H h] by fact
+  interpret vectorspace [E] by fact
+  show ?thesis proof
+    note E = `vectorspace E`
+    have H': "vectorspace H'"
+    proof (unfold H'_def)
+      from `x0 \<in> E`
+      have "lin x0 \<unlhd> E" ..
+      with HE show "vectorspace (H + lin x0)" using E ..
+    qed
+    {
+      fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
+      show "h' (x1 + x2) = h' x1 + h' x2"
+      proof -
+	from H' x1 x2 have "x1 + x2 \<in> H'"
+          by (rule vectorspace.add_closed)
+	with x1 x2 obtain y y1 y2 a a1 a2 where
+          x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
           and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
           and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
-        by (unfold H'_def sum_def lin_def) blast
-
-      have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
-      proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
-        from HE y1 y2 show "y1 + y2 \<in> H"
-          by (rule subspace.add_closed)
-        from x0 and HE y y1 y2
-        have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
-        with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
-          by (simp add: add_ac add_mult_distrib2)
-        also note x1x2
-        finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
+          by (unfold H'_def sum_def lin_def) blast
+	
+	have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
+	proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
+          from HE y1 y2 show "y1 + y2 \<in> H"
+            by (rule subspace.add_closed)
+          from x0 and HE y y1 y2
+          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
+          with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
+            by (simp add: add_ac add_mult_distrib2)
+          also note x1x2
+          finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
+	qed
+	
+	from h'_def x1x2 E HE y x0
+	have "h' (x1 + x2) = h y + a * xi"
+          by (rule h'_definite)
+	also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
+          by (simp only: ya)
+	also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
+          by simp
+	also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
+          by (simp add: left_distrib)
+	also from h'_def x1_rep E HE y1 x0
+	have "h y1 + a1 * xi = h' x1"
+          by (rule h'_definite [symmetric])
+	also from h'_def x2_rep E HE y2 x0
+	have "h y2 + a2 * xi = h' x2"
+          by (rule h'_definite [symmetric])
+	finally show ?thesis .
       qed
-
-      from h'_def x1x2 E HE y x0
-      have "h' (x1 + x2) = h y + a * xi"
-        by (rule h'_definite)
-      also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
-        by (simp only: ya)
-      also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
-        by simp
-      also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
-        by (simp add: left_distrib)
-      also from h'_def x1_rep E HE y1 x0
-      have "h y1 + a1 * xi = h' x1"
-        by (rule h'_definite [symmetric])
-      also from h'_def x2_rep E HE y2 x0
-      have "h y2 + a2 * xi = h' x2"
-        by (rule h'_definite [symmetric])
-      finally show ?thesis .
-    qed
-  next
-    fix x1 c assume x1: "x1 \<in> H'"
-    show "h' (c \<cdot> x1) = c * (h' x1)"
-    proof -
-      from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
-        by (rule vectorspace.mult_closed)
-      with x1 obtain y a y1 a1 where
-            cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
+    next
+      fix x1 c assume x1: "x1 \<in> H'"
+      show "h' (c \<cdot> x1) = c * (h' x1)"
+      proof -
+	from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
+          by (rule vectorspace.mult_closed)
+	with x1 obtain y a y1 a1 where
+          cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
           and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
-        by (unfold H'_def sum_def lin_def) blast
-
-      have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
-      proof (rule decomp_H')
-        from HE y1 show "c \<cdot> y1 \<in> H"
-          by (rule subspace.mult_closed)
-        from x0 and HE y y1
-        have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
-        with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
-          by (simp add: mult_assoc add_mult_distrib1)
-        also note cx1_rep
-        finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
+          by (unfold H'_def sum_def lin_def) blast
+	
+	have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
+	proof (rule decomp_H')
+          from HE y1 show "c \<cdot> y1 \<in> H"
+            by (rule subspace.mult_closed)
+          from x0 and HE y y1
+          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
+          with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
+            by (simp add: mult_assoc add_mult_distrib1)
+          also note cx1_rep
+          finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
+	qed
+	
+	from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
+          by (rule h'_definite)
+	also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
+          by (simp only: ya)
+	also from y1 have "h (c \<cdot> y1) = c * h y1"
+          by simp
+	also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
+          by (simp only: right_distrib)
+	also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
+          by (rule h'_definite [symmetric])
+	finally show ?thesis .
       qed
-
-      from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
-        by (rule h'_definite)
-      also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
-        by (simp only: ya)
-      also from y1 have "h (c \<cdot> y1) = c * h y1"
-        by simp
-      also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
-        by (simp only: right_distrib)
-      also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
-        by (rule h'_definite [symmetric])
-      finally show ?thesis .
-    qed
-  }
+    }
+  qed
 qed
 
 text {* \medskip The linear extension @{text h'} of @{text h}
   is bounded by the seminorm @{text p}. *}
 
 lemma h'_norm_pres:
-  includes var H + var h + var E
   assumes 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' \<equiv> H + lin x0"
     and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
-  includes vectorspace E + subspace H E + seminorm E p + linearform H h
+  assumes E: "vectorspace E" and HE: "subspace H E"
+    and "seminorm E p" and "linearform H h"
   assumes a: "\<forall>y \<in> H. h y \<le> p y"
     and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
   shows "\<forall>x \<in> H'. h' x \<le> p x"
-proof
-  note E = `vectorspace E`
-  note HE = `subspace H E`
-  fix x assume x': "x \<in> H'"
-  show "h' x \<le> p x"
-  proof -
-    from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
-      and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
-    from x' obtain y a where
+proof -
+  interpret vectorspace [E] by fact
+  interpret subspace [H E] by fact
+  interpret seminorm [E p] by fact
+  interpret linearform [H h] by fact
+  show ?thesis proof
+    fix x assume x': "x \<in> H'"
+    show "h' x \<le> p x"
+    proof -
+      from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
+	and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
+      from x' obtain y a where
         x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
-      by (unfold H'_def sum_def lin_def) blast
-    from y have y': "y \<in> E" ..
-    from y have ay: "inverse a \<cdot> y \<in> H" by simp
-
-    from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
-      by (rule h'_definite)
-    also have "\<dots> \<le> p (y + a \<cdot> x0)"
-    proof (rule linorder_cases)
-      assume z: "a = 0"
-      then have "h y + a * xi = h y" by simp
-      also from a y have "\<dots> \<le> p y" ..
-      also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
-      finally show ?thesis .
-    next
-      txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
-        with @{text ya} taken as @{text "y / a"}: *}
-      assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
-      from a1 ay
-      have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
-      with lz have "a * xi \<le>
+	by (unfold H'_def sum_def lin_def) blast
+      from y have y': "y \<in> E" ..
+      from y have ay: "inverse a \<cdot> y \<in> H" by simp
+      
+      from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
+	by (rule h'_definite)
+      also have "\<dots> \<le> p (y + a \<cdot> x0)"
+      proof (rule linorder_cases)
+	assume z: "a = 0"
+	then have "h y + a * xi = h y" by simp
+	also from a y have "\<dots> \<le> p y" ..
+	also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
+	finally show ?thesis .
+      next
+	txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
+          with @{text ya} taken as @{text "y / a"}: *}
+	assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
+	from a1 ay
+	have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
+	with lz have "a * xi \<le>
           a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
-        by (simp add: mult_left_mono_neg order_less_imp_le)
-
-      also have "\<dots> =
+          by (simp add: mult_left_mono_neg order_less_imp_le)
+	
+	also have "\<dots> =
           - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
-	by (simp add: right_diff_distrib)
-      also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
+	  by (simp add: right_diff_distrib)
+	also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
           p (a \<cdot> (inverse a \<cdot> y + x0))"
-        by (simp add: abs_homogenous)
-      also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
-        by (simp add: add_mult_distrib1 mult_assoc [symmetric])
-      also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
-        by simp
-      finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
-      then show ?thesis by simp
-    next
-      txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
-        with @{text ya} taken as @{text "y / a"}: *}
-      assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
-      from a2 ay
-      have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
-      with gz have "a * xi \<le>
+          by (simp add: abs_homogenous)
+	also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
+          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
+	also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
+          by simp
+	finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
+	then show ?thesis by simp
+      next
+	txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
+          with @{text ya} taken as @{text "y / a"}: *}
+	assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
+	from a2 ay
+	have "xi \<le> 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 simp
-      also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
-	by (simp add: right_diff_distrib)
-      also from gz x0 y'
-      have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
-        by (simp add: abs_homogenous)
-      also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
-        by (simp add: add_mult_distrib1 mult_assoc [symmetric])
-      also from nz y have "a * h (inverse a \<cdot> y) = h y"
-        by simp
-      finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
-      then show ?thesis by simp
+          by simp
+	also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
+	  by (simp add: right_diff_distrib)
+	also from gz x0 y'
+	have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
+          by (simp add: abs_homogenous)
+	also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
+          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
+	also from nz y have "a * h (inverse a \<cdot> y) = h y"
+          by simp
+	finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
+	then show ?thesis by simp
+      qed
+      also from x_rep have "\<dots> = p x" by (simp only:)
+      finally show ?thesis .
     qed
-    also from x_rep have "\<dots> = p x" by (simp only:)
-    finally show ?thesis .
   qed
 qed
 
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -399,9 +399,14 @@
 *}
 
 lemma abs_ineq_iff:
-  includes subspace H E + vectorspace E + seminorm E p + linearform H h
+  assumes "subspace H E" and "vectorspace E" and "seminorm E p"
+    and "linearform H h"
   shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
 proof
+  interpret subspace [H E] by fact
+  interpret vectorspace [E] by fact
+  interpret seminorm [E p] by fact
+  interpret linearform [H h] by fact
   have H: "vectorspace H" using `vectorspace E` ..
   {
     assume l: ?L
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -20,9 +20,10 @@
 declare linearform.intro [intro?]
 
 lemma (in linearform) neg [iff]:
-  includes vectorspace
+  assumes "vectorspace V"
   shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
 proof -
+  interpret vectorspace [V] by fact
   assume x: "x \<in> V"
   hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
   also from x have "... = (- 1) * (f x)" by (rule mult)
@@ -31,9 +32,10 @@
 qed
 
 lemma (in linearform) diff [iff]:
-  includes vectorspace
+  assumes "vectorspace V"
   shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
 proof -
+  interpret vectorspace [V] by fact
   assume x: "x \<in> V" and y: "y \<in> V"
   hence "x - y = x + - y" by (rule diff_eq1)
   also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)
@@ -44,9 +46,10 @@
 text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
 
 lemma (in linearform) zero [iff]:
-  includes vectorspace
+  assumes "vectorspace V"
   shows "f 0 = 0"
 proof -
+  interpret vectorspace [V] by fact
   have "f 0 = f (0 - 0)" by simp
   also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
   also have "\<dots> = 0" by simp
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -27,9 +27,10 @@
 declare seminorm.intro [intro?]
 
 lemma (in seminorm) diff_subadditive:
-  includes vectorspace
+  assumes "vectorspace V"
   shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
 proof -
+  interpret vectorspace [V] by fact
   assume x: "x \<in> V" and y: "y \<in> V"
   hence "x - y = x + - 1 \<cdot> y"
     by (simp add: diff_eq2 negate_eq2a)
@@ -42,9 +43,10 @@
 qed
 
 lemma (in seminorm) minus:
-  includes vectorspace
+  assumes "vectorspace V"
   shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
 proof -
+  interpret vectorspace [V] by fact
   assume x: "x \<in> V"
   hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
   also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
@@ -95,14 +97,19 @@
 *}
 
 lemma subspace_normed_vs [intro?]:
-  includes subspace F E + normed_vectorspace E
+  fixes F E norm
+  assumes "subspace F E" "normed_vectorspace E norm"
   shows "normed_vectorspace F norm"
-proof
-  show "vectorspace F" by (rule vectorspace) unfold_locales
-next
-  have "NormedSpace.norm E norm" by unfold_locales
-  with subset show "NormedSpace.norm F norm"
-    by (simp add: norm_def seminorm_def norm_axioms_def)
+proof -
+  interpret subspace [F E] by fact
+  interpret normed_vectorspace [E norm] by fact
+  show ?thesis proof
+    show "vectorspace F" by (rule vectorspace) unfold_locales
+  next
+    have "NormedSpace.norm E norm" by unfold_locales
+    with subset show "NormedSpace.norm F norm"
+      by (simp add: norm_def seminorm_def norm_axioms_def)
+  qed
 qed
 
 end
diff -r 8882d47e075f -r 2c01c0bdb385 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -41,10 +41,12 @@
   by (rule subspace.subsetD)
 
 lemma (in subspace) diff_closed [iff]:
-  includes vectorspace
-  shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U"
-  by (simp add: diff_eq1 negate_eq1)
-
+  assumes "vectorspace V"
+  shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U" (is "PROP ?P")
+proof -
+  interpret vectorspace [V] by fact
+  show "PROP ?P" by (simp add: diff_eq1 negate_eq1)
+qed
 
 text {*
   \medskip Similar as for linear spaces, the existence of the zero
@@ -53,9 +55,10 @@
 *}
 
 lemma (in subspace) zero [intro]:
-  includes vectorspace
+  assumes "vectorspace V"
   shows "0 \<in> U"
 proof -
+  interpret vectorspace [V] by fact
   have "U \<noteq> {}" by (rule U_V.non_empty)
   then obtain x where x: "x \<in> U" by blast
   hence "x \<in> V" .. hence "0 = x - x" by simp
@@ -64,32 +67,37 @@
 qed
 
 lemma (in subspace) neg_closed [iff]:
-  includes vectorspace
-  shows "x \<in> U \<Longrightarrow> - x \<in> U"
-  by (simp add: negate_eq1)
-
+  assumes "vectorspace V"
+  shows "x \<in> U \<Longrightarrow> - x \<in> U" (is "PROP ?P")
+proof -
+  interpret vectorspace [V] by fact
+  show "PROP ?P" by (simp add: negate_eq1)
+qed
 
 text {* \medskip Further derived laws: every subspace is a vector space. *}
 
 lemma (in subspace) vectorspace [iff]:
-  includes vectorspace
+  assumes "vectorspace V"
   shows "vectorspace U"
-proof
-  show "U \<noteq> {}" ..
-  fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
-  fix a b :: real
-  from x y show "x + y \<in> U" by simp
-  from x show "a \<cdot> x \<in> U" by simp
-  from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)
-  from x y show "x + y = y + x" by (simp add: add_ac)
-  from x show "x - x = 0" by simp
-  from x show "0 + x = x" by simp
-  from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib)
-  from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib)
-  from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc)
-  from x show "1 \<cdot> x = x" by simp
-  from x show "- x = - 1 \<cdot> x" by (simp add: negate_eq1)
-  from x y show "x - y = x + - y" by (simp add: diff_eq1)
+proof -
+  interpret vectorspace [V] by fact
+  show ?thesis proof
+    show "U \<noteq> {}" ..
+    fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
+    fix a b :: real
+    from x y show "x + y \<in> U" by simp
+    from x show "a \<cdot> x \<in> U" by simp
+    from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)
+    from x y show "x + y = y + x" by (simp add: add_ac)
+    from x show "x - x = 0" by simp
+    from x show "0 + x = x" by simp
+    from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib)
+    from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib)
+    from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc)
+    from x show "1 \<cdot> x = x" by simp
+    from x show "- x = - 1 \<cdot> x" by (simp add: negate_eq1)
+    from x y show "x - y = x + - y" by (simp add: diff_eq1)
+  qed
 qed
 
 
@@ -236,61 +244,70 @@
 text {* @{text U} is a subspace of @{text "U + V"}. *}
 
 lemma subspace_sum1 [iff]:
-  includes vectorspace U + vectorspace V
+  assumes "vectorspace U" "vectorspace V"
   shows "U \<unlhd> U + V"
-proof
-  show "U \<noteq> {}" ..
-  show "U \<subseteq> U + V"
-  proof
-    fix x assume x: "x \<in> U"
-    moreover have "0 \<in> V" ..
-    ultimately have "x + 0 \<in> U + V" ..
-    with x show "x \<in> U + V" by simp
+proof -
+  interpret vectorspace [U] by fact
+  interpret vectorspace [V] by fact
+  show ?thesis proof
+    show "U \<noteq> {}" ..
+    show "U \<subseteq> U + V"
+    proof
+      fix x assume x: "x \<in> U"
+      moreover have "0 \<in> V" ..
+      ultimately have "x + 0 \<in> U + V" ..
+      with x show "x \<in> U + V" by simp
+    qed
+    fix x y assume x: "x \<in> U" and "y \<in> U"
+    thus "x + y \<in> U" by simp
+    from x show "\<And>a. a \<cdot> x \<in> U" by simp
   qed
-  fix x y assume x: "x \<in> U" and "y \<in> U"
-  thus "x + y \<in> U" by simp
-  from x show "\<And>a. a \<cdot> x \<in> U" by simp
 qed
 
 text {* The sum of two subspaces is again a subspace. *}
 
 lemma sum_subspace [intro?]:
-  includes subspace U E + vectorspace E + subspace V E
+  assumes "subspace U E" "vectorspace E" "subspace V E"
   shows "U + V \<unlhd> E"
-proof
-  have "0 \<in> U + V"
-  proof
-    show "0 \<in> U" using `vectorspace E` ..
-    show "0 \<in> V" using `vectorspace E` ..
-    show "(0::'a) = 0 + 0" by simp
-  qed
-  thus "U + V \<noteq> {}" by blast
-  show "U + V \<subseteq> E"
-  proof
-    fix x assume "x \<in> U + V"
-    then obtain u v where "x = u + v" and
-      "u \<in> U" and "v \<in> V" ..
-    then show "x \<in> E" by simp
-  qed
-  fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
-  show "x + y \<in> U + V"
-  proof -
-    from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
-    moreover
-    from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" ..
-    ultimately
-    have "ux + uy \<in> U"
-      and "vx + vy \<in> V"
-      and "x + y = (ux + uy) + (vx + vy)"
-      using x y by (simp_all add: add_ac)
-    thus ?thesis ..
-  qed
-  fix a show "a \<cdot> x \<in> U + V"
-  proof -
-    from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
-    hence "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
-      and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)
-    thus ?thesis ..
+proof -
+  interpret subspace [U E] by fact
+  interpret vectorspace [E] by fact
+  interpret subspace [V E] by fact
+  show ?thesis proof
+    have "0 \<in> U + V"
+    proof
+      show "0 \<in> U" using `vectorspace E` ..
+      show "0 \<in> V" using `vectorspace E` ..
+      show "(0::'a) = 0 + 0" by simp
+    qed
+    thus "U + V \<noteq> {}" by blast
+    show "U + V \<subseteq> E"
+    proof
+      fix x assume "x \<in> U + V"
+      then obtain u v where "x = u + v" and
+	"u \<in> U" and "v \<in> V" ..
+      then show "x \<in> E" by simp
+    qed
+    fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
+    show "x + y \<in> U + V"
+    proof -
+      from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
+      moreover
+      from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" ..
+      ultimately
+      have "ux + uy \<in> U"
+	and "vx + vy \<in> V"
+	and "x + y = (ux + uy) + (vx + vy)"
+	using x y by (simp_all add: add_ac)
+      thus ?thesis ..
+    qed
+    fix a show "a \<cdot> x \<in> U + V"
+    proof -
+      from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
+      hence "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
+	and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)
+      thus ?thesis ..
+    qed
   qed
 qed
 
@@ -312,37 +329,42 @@
 *}
 
 lemma decomp:
-  includes vectorspace E + subspace U E + subspace V E
+  assumes "vectorspace E" "subspace U E" "subspace V E"
   assumes direct: "U \<inter> V = {0}"
     and u1: "u1 \<in> U" and u2: "u2 \<in> U"
     and v1: "v1 \<in> V" and v2: "v2 \<in> V"
     and sum: "u1 + v1 = u2 + v2"
   shows "u1 = u2 \<and> v1 = v2"
-proof
-  have U: "vectorspace U"
-    using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
-  have V: "vectorspace V"
-    using `subspace V E` `vectorspace E` by (rule subspace.vectorspace)
-  from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
-    by (simp add: add_diff_swap)
-  from u1 u2 have u: "u1 - u2 \<in> U"
-    by (rule vectorspace.diff_closed [OF U])
-  with eq have v': "v2 - v1 \<in> U" by (simp only:)
-  from v2 v1 have v: "v2 - v1 \<in> V"
-    by (rule vectorspace.diff_closed [OF V])
-  with eq have u': " u1 - u2 \<in> V" by (simp only:)
-
-  show "u1 = u2"
-  proof (rule add_minus_eq)
-    from u1 show "u1 \<in> E" ..
-    from u2 show "u2 \<in> E" ..
-    from u u' and direct show "u1 - u2 = 0" by blast
-  qed
-  show "v1 = v2"
-  proof (rule add_minus_eq [symmetric])
-    from v1 show "v1 \<in> E" ..
-    from v2 show "v2 \<in> E" ..
-    from v v' and direct show "v2 - v1 = 0" by blast
+proof -
+  interpret vectorspace [E] by fact
+  interpret subspace [U E] by fact
+  interpret subspace [V E] by fact
+  show ?thesis proof
+    have U: "vectorspace U"  (* FIXME: use interpret *)
+      using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
+    have V: "vectorspace V"
+      using `subspace V E` `vectorspace E` by (rule subspace.vectorspace)
+    from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
+      by (simp add: add_diff_swap)
+    from u1 u2 have u: "u1 - u2 \<in> U"
+      by (rule vectorspace.diff_closed [OF U])
+    with eq have v': "v2 - v1 \<in> U" by (simp only:)
+    from v2 v1 have v: "v2 - v1 \<in> V"
+      by (rule vectorspace.diff_closed [OF V])
+    with eq have u': " u1 - u2 \<in> V" by (simp only:)
+    
+    show "u1 = u2"
+    proof (rule add_minus_eq)
+      from u1 show "u1 \<in> E" ..
+      from u2 show "u2 \<in> E" ..
+      from u u' and direct show "u1 - u2 = 0" by blast
+    qed
+    show "v1 = v2"
+    proof (rule add_minus_eq [symmetric])
+      from v1 show "v1 \<in> E" ..
+      from v2 show "v2 \<in> E" ..
+      from v v' and direct show "v2 - v1 = 0" by blast
+    qed
   qed
 qed
 
@@ -356,48 +378,52 @@
 *}
 
 lemma decomp_H':
-  includes vectorspace E + subspace H E
+  assumes "vectorspace E" "subspace H E"
   assumes y1: "y1 \<in> H" and y2: "y2 \<in> H"
     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
     and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
   shows "y1 = y2 \<and> a1 = a2"
-proof
-  have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
-  proof (rule decomp)
-    show "a1 \<cdot> x' \<in> lin x'" ..
-    show "a2 \<cdot> x' \<in> lin x'" ..
-    show "H \<inter> lin x' = {0}"
-    proof
-      show "H \<inter> lin x' \<subseteq> {0}"
+proof -
+  interpret vectorspace [E] by fact
+  interpret subspace [H E] by fact
+  show ?thesis proof
+    have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
+    proof (rule decomp)
+      show "a1 \<cdot> x' \<in> lin x'" ..
+      show "a2 \<cdot> x' \<in> lin x'" ..
+      show "H \<inter> lin x' = {0}"
       proof
-        fix x assume x: "x \<in> H \<inter> lin x'"
-        then obtain a where xx': "x = a \<cdot> x'"
-          by blast
-        have "x = 0"
-        proof cases
-          assume "a = 0"
-          with xx' and x' show ?thesis by simp
-        next
-          assume a: "a \<noteq> 0"
-          from x have "x \<in> H" ..
-          with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
-          with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
-          with `x' \<notin> H` show ?thesis by contradiction
-        qed
-        thus "x \<in> {0}" ..
+	show "H \<inter> lin x' \<subseteq> {0}"
+	proof
+          fix x assume x: "x \<in> H \<inter> lin x'"
+          then obtain a where xx': "x = a \<cdot> x'"
+            by blast
+          have "x = 0"
+          proof cases
+            assume "a = 0"
+            with xx' and x' show ?thesis by simp
+          next
+            assume a: "a \<noteq> 0"
+            from x have "x \<in> H" ..
+            with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
+            with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
+            with `x' \<notin> H` show ?thesis by contradiction
+          qed
+          thus "x \<in> {0}" ..
+	qed
+	show "{0} \<subseteq> H \<inter> lin x'"
+	proof -
+          have "0 \<in> H" using `vectorspace E` ..
+          moreover have "0 \<in> lin x'" using `x' \<in> E` ..
+          ultimately show ?thesis by blast
+	qed
       qed
-      show "{0} \<subseteq> H \<inter> lin x'"
-      proof -
-        have "0 \<in> H" using `vectorspace E` ..
-        moreover have "0 \<in> lin x'" using `x' \<in> E` ..
-        ultimately show ?thesis by blast
-      qed
-    qed
-    show "lin x' \<unlhd> E" using `x' \<in> E` ..
-  qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
-  thus "y1 = y2" ..
-  from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
-  with x' show "a1 = a2" by (simp add: mult_right_cancel)
+      show "lin x' \<unlhd> E" using `x' \<in> E` ..
+    qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
+    thus "y1 = y2" ..
+    from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
+    with x' show "a1 = a2" by (simp add: mult_right_cancel)
+  qed
 qed
 
 text {*
@@ -408,19 +434,23 @@
 *}
 
 lemma decomp_H'_H:
-  includes vectorspace E + subspace H E
+  assumes "vectorspace E" "subspace H E"
   assumes t: "t \<in> H"
     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
-proof (rule, simp_all only: split_paired_all split_conv)
-  from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
-  fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"
-  have "y = t \<and> a = 0"
-  proof (rule decomp_H')
-    from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
-    from ya show "y \<in> H" ..
-  qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
-  with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
+proof -
+  interpret vectorspace [E] by fact
+  interpret subspace [H E] by fact
+  show ?thesis proof (rule, simp_all only: split_paired_all split_conv)
+    from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
+    fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"
+    have "y = t \<and> a = 0"
+    proof (rule decomp_H')
+      from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
+      from ya show "y \<in> H" ..
+    qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
+    with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
+  qed
 qed
 
 text {*
@@ -430,16 +460,18 @@
 *}
 
 lemma h'_definite:
-  includes var H
+  fixes H
   assumes 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)"
     and x: "x = y + a \<cdot> x'"
-  includes vectorspace E + subspace H E
+  assumes "vectorspace E" "subspace H E"
   assumes y: "y \<in> H"
     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   shows "h' x = h y + a * xi"
 proof -
+  interpret vectorspace [E] by fact
+  interpret subspace [H E] by fact
   from x y x' have "x \<in> H + lin x'" by auto
   have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
   proof (rule ex_ex1I)