More porting to new locales.
authorballarin
Mon Dec 15 18:12:52 2008 +0100 (2008-12-15)
changeset 2923460f7fb56f8cd
parent 29233 ce6d35a0bed6
child 29235 2d62b637fa80
More porting to new locales.
src/HOL/NSA/StarDef.thy
src/HOL/Real/HahnBanach/Bounds.thy
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
src/HOL/Real/HahnBanach/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/Real/HahnBanach/ZornLemma.thy
src/HOL/Word/TdThs.thy
src/HOL/Word/WordDefinition.thy
src/HOL/ex/Abstract_NAT.thy
src/HOL/ex/Tarski.thy
src/HOL/plain.ML
     1.1 --- a/src/HOL/NSA/StarDef.thy	Sun Dec 14 18:45:51 2008 +0100
     1.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Dec 15 18:12:52 2008 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  apply (rule nat_infinite)
     1.5  done
     1.6  
     1.7 -interpretation FreeUltrafilterNat: freeultrafilter [FreeUltrafilterNat]
     1.8 +interpretation FreeUltrafilterNat!: freeultrafilter FreeUltrafilterNat
     1.9  by (rule freeultrafilter_FreeUltrafilterNat)
    1.10  
    1.11  text {* This rule takes the place of the old ultra tactic *}
     2.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Sun Dec 14 18:45:51 2008 +0100
     2.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Mon Dec 15 18:12:52 2008 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Real/HahnBanach/Bounds.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Gertrud Bauer, TU Munich
     2.7  *)
     2.8  
     2.9 @@ -27,7 +26,7 @@
    2.10    assumes "lub A x"
    2.11    shows "\<Squnion>A = (x::'a::order)"
    2.12  proof -
    2.13 -  interpret lub [A x] by fact
    2.14 +  interpret lub A x by fact
    2.15    show ?thesis
    2.16    proof (unfold the_lub_def)
    2.17      from `lub A x` show "The (lub A) = x"
     3.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sun Dec 14 18:45:51 2008 +0100
     3.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Dec 15 18:12:52 2008 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOL/Real/HahnBanach/FunctionNorm.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Gertrud Bauer, TU Munich
     3.7  *)
     3.8  
     3.9 @@ -22,7 +21,7 @@
    3.10    linear forms:
    3.11  *}
    3.12  
    3.13 -locale continuous = var V + norm_syntax + linearform +
    3.14 +locale continuous = var_V + norm_syntax + linearform +
    3.15    assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
    3.16  
    3.17  declare continuous.intro [intro?] continuous_axioms.intro [intro?]
    3.18 @@ -91,7 +90,7 @@
    3.19    assumes "continuous V norm f"
    3.20    shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    3.21  proof -
    3.22 -  interpret continuous [V norm f] by fact
    3.23 +  interpret continuous V norm f by fact
    3.24    txt {* The existence of the supremum is shown using the
    3.25      completeness of the reals. Completeness means, that every
    3.26      non-empty bounded set of reals has a supremum. *}
    3.27 @@ -159,7 +158,7 @@
    3.28    assumes b: "b \<in> B V f"
    3.29    shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
    3.30  proof -
    3.31 -  interpret continuous [V norm f] by fact
    3.32 +  interpret continuous V norm f by fact
    3.33    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    3.34      using `continuous V norm f` by (rule fn_norm_works)
    3.35    from this and b show ?thesis ..
    3.36 @@ -170,7 +169,7 @@
    3.37    assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
    3.38    shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
    3.39  proof -
    3.40 -  interpret continuous [V norm f] by fact
    3.41 +  interpret continuous V norm f by fact
    3.42    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    3.43      using `continuous V norm f` by (rule fn_norm_works)
    3.44    from this and b show ?thesis ..
    3.45 @@ -182,7 +181,7 @@
    3.46    assumes "continuous V norm f"
    3.47    shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
    3.48  proof -
    3.49 -  interpret continuous [V norm f] by fact
    3.50 +  interpret continuous V norm f by fact
    3.51    txt {* The function norm is defined as the supremum of @{text B}.
    3.52      So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
    3.53      0"}, provided the supremum exists and @{text B} is not empty. *}
    3.54 @@ -204,8 +203,8 @@
    3.55    assumes x: "x \<in> V"
    3.56    shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
    3.57  proof -
    3.58 -  interpret continuous [V norm f] by fact
    3.59 -  interpret linearform [V f] .
    3.60 +  interpret continuous V norm f by fact
    3.61 +  interpret linearform V f .
    3.62    show ?thesis
    3.63    proof cases
    3.64      assume "x = 0"
    3.65 @@ -246,7 +245,7 @@
    3.66    assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
    3.67    shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
    3.68  proof -
    3.69 -  interpret continuous [V norm f] by fact
    3.70 +  interpret continuous V norm f by fact
    3.71    show ?thesis
    3.72    proof (rule fn_norm_leastB [folded B_def fn_norm_def])
    3.73      fix b assume b: "b \<in> B V f"
     4.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Sun Dec 14 18:45:51 2008 +0100
     4.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Dec 15 18:12:52 2008 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Gertrud Bauer, TU Munich
     4.7  *)
     4.8  
     4.9 @@ -63,10 +62,10 @@
    4.10      -- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *}
    4.11      -- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *}
    4.12  proof -
    4.13 -  interpret vectorspace [E] by fact
    4.14 -  interpret subspace [F E] by fact
    4.15 -  interpret seminorm [E p] by fact
    4.16 -  interpret linearform [F f] by fact
    4.17 +  interpret vectorspace E by fact
    4.18 +  interpret subspace F E by fact
    4.19 +  interpret seminorm E p by fact
    4.20 +  interpret linearform F f by fact
    4.21    def M \<equiv> "norm_pres_extensions E p F f"
    4.22    then have M: "M = \<dots>" by (simp only:)
    4.23    from E have F: "vectorspace F" ..
    4.24 @@ -322,10 +321,10 @@
    4.25      \<and> (\<forall>x \<in> F. g x = f x)
    4.26      \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
    4.27  proof -
    4.28 -  interpret vectorspace [E] by fact
    4.29 -  interpret subspace [F E] by fact
    4.30 -  interpret linearform [F f] by fact
    4.31 -  interpret seminorm [E p] by fact
    4.32 +  interpret vectorspace E by fact
    4.33 +  interpret subspace F E by fact
    4.34 +  interpret linearform F f by fact
    4.35 +  interpret seminorm E p by fact
    4.36    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)"
    4.37      using E FE sn lf
    4.38    proof (rule HahnBanach)
    4.39 @@ -363,12 +362,12 @@
    4.40       \<and> (\<forall>x \<in> F. g x = f x)
    4.41       \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
    4.42  proof -
    4.43 -  interpret normed_vectorspace [E norm] by fact
    4.44 -  interpret normed_vectorspace_with_fn_norm [E norm B fn_norm]
    4.45 +  interpret normed_vectorspace E norm by fact
    4.46 +  interpret normed_vectorspace_with_fn_norm E norm B fn_norm
    4.47      by (auto simp: B_def fn_norm_def) intro_locales
    4.48 -  interpret subspace [F E] by fact
    4.49 -  interpret linearform [F f] by fact
    4.50 -  interpret continuous [F norm f] by fact
    4.51 +  interpret subspace F E by fact
    4.52 +  interpret linearform F f by fact
    4.53 +  interpret continuous F norm f by fact
    4.54    have E: "vectorspace E" by intro_locales
    4.55    have F: "vectorspace F" by rule intro_locales
    4.56    have F_norm: "normed_vectorspace F norm"
     5.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Sun Dec 14 18:45:51 2008 +0100
     5.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Dec 15 18:12:52 2008 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Gertrud Bauer, TU Munich
     5.7  *)
     5.8  
     5.9 @@ -46,7 +45,7 @@
    5.10    assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
    5.11    shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
    5.12  proof -
    5.13 -  interpret vectorspace [F] by fact
    5.14 +  interpret vectorspace F by fact
    5.15    txt {* From the completeness of the reals follows:
    5.16      The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
    5.17      non-empty and has an upper bound. *}
    5.18 @@ -98,8 +97,8 @@
    5.19    assumes E: "vectorspace E"
    5.20    shows "linearform H' h'"
    5.21  proof -
    5.22 -  interpret linearform [H h] by fact
    5.23 -  interpret vectorspace [E] by fact
    5.24 +  interpret linearform H h by fact
    5.25 +  interpret vectorspace E by fact
    5.26    show ?thesis
    5.27    proof
    5.28      note E = `vectorspace E`
    5.29 @@ -203,10 +202,10 @@
    5.30      and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
    5.31    shows "\<forall>x \<in> H'. h' x \<le> p x"
    5.32  proof -
    5.33 -  interpret vectorspace [E] by fact
    5.34 -  interpret subspace [H E] by fact
    5.35 -  interpret seminorm [E p] by fact
    5.36 -  interpret linearform [H h] by fact
    5.37 +  interpret vectorspace E by fact
    5.38 +  interpret subspace H E by fact
    5.39 +  interpret seminorm E p by fact
    5.40 +  interpret linearform H h by fact
    5.41    show ?thesis
    5.42    proof
    5.43      fix x assume x': "x \<in> H'"
     6.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Sun Dec 14 18:45:51 2008 +0100
     6.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Dec 15 18:12:52 2008 +0100
     6.3 @@ -405,10 +405,10 @@
     6.4      and "linearform H h"
     6.5    shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
     6.6  proof
     6.7 -  interpret subspace [H E] by fact
     6.8 -  interpret vectorspace [E] by fact
     6.9 -  interpret seminorm [E p] by fact
    6.10 -  interpret linearform [H h] by fact
    6.11 +  interpret subspace H E by fact
    6.12 +  interpret vectorspace E by fact
    6.13 +  interpret seminorm E p by fact
    6.14 +  interpret linearform H h by fact
    6.15    have H: "vectorspace H" using `vectorspace E` ..
    6.16    {
    6.17      assume l: ?L
     7.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Sun Dec 14 18:45:51 2008 +0100
     7.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Mon Dec 15 18:12:52 2008 +0100
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      HOL/Real/HahnBanach/Linearform.thy
     7.5 -    ID:         $Id$
     7.6      Author:     Gertrud Bauer, TU Munich
     7.7  *)
     7.8  
     7.9 @@ -14,8 +13,8 @@
    7.10    that is additive and multiplicative.
    7.11  *}
    7.12  
    7.13 -locale linearform = var V + var f +
    7.14 -  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
    7.15 +locale linearform =
    7.16 +  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f
    7.17    assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
    7.18      and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
    7.19  
    7.20 @@ -25,7 +24,7 @@
    7.21    assumes "vectorspace V"
    7.22    shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
    7.23  proof -
    7.24 -  interpret vectorspace [V] by fact
    7.25 +  interpret vectorspace V by fact
    7.26    assume x: "x \<in> V"
    7.27    then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
    7.28    also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
    7.29 @@ -37,7 +36,7 @@
    7.30    assumes "vectorspace V"
    7.31    shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
    7.32  proof -
    7.33 -  interpret vectorspace [V] by fact
    7.34 +  interpret vectorspace V by fact
    7.35    assume x: "x \<in> V" and y: "y \<in> V"
    7.36    then have "x - y = x + - y" by (rule diff_eq1)
    7.37    also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
    7.38 @@ -51,7 +50,7 @@
    7.39    assumes "vectorspace V"
    7.40    shows "f 0 = 0"
    7.41  proof -
    7.42 -  interpret vectorspace [V] by fact
    7.43 +  interpret vectorspace V by fact
    7.44    have "f 0 = f (0 - 0)" by simp
    7.45    also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
    7.46    also have "\<dots> = 0" by simp
     8.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Sun Dec 14 18:45:51 2008 +0100
     8.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Dec 15 18:12:52 2008 +0100
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      HOL/Real/HahnBanach/NormedSpace.thy
     8.5 -    ID:         $Id$
     8.6      Author:     Gertrud Bauer, TU Munich
     8.7  *)
     8.8  
     8.9 @@ -20,7 +19,7 @@
    8.10  locale norm_syntax =
    8.11    fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
    8.12  
    8.13 -locale seminorm = var V + norm_syntax +
    8.14 +locale seminorm = var_V + norm_syntax +
    8.15    constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
    8.16    assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
    8.17      and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
    8.18 @@ -32,7 +31,7 @@
    8.19    assumes "vectorspace V"
    8.20    shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    8.21  proof -
    8.22 -  interpret vectorspace [V] by fact
    8.23 +  interpret vectorspace V by fact
    8.24    assume x: "x \<in> V" and y: "y \<in> V"
    8.25    then have "x - y = x + - 1 \<cdot> y"
    8.26      by (simp add: diff_eq2 negate_eq2a)
    8.27 @@ -48,7 +47,7 @@
    8.28    assumes "vectorspace V"
    8.29    shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
    8.30  proof -
    8.31 -  interpret vectorspace [V] by fact
    8.32 +  interpret vectorspace V by fact
    8.33    assume x: "x \<in> V"
    8.34    then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
    8.35    also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
    8.36 @@ -103,8 +102,8 @@
    8.37    assumes "subspace F E" "normed_vectorspace E norm"
    8.38    shows "normed_vectorspace F norm"
    8.39  proof -
    8.40 -  interpret subspace [F E] by fact
    8.41 -  interpret normed_vectorspace [E norm] by fact
    8.42 +  interpret subspace F E by fact
    8.43 +  interpret normed_vectorspace E norm by fact
    8.44    show ?thesis
    8.45    proof
    8.46      show "vectorspace F" by (rule vectorspace) unfold_locales
     9.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Sun Dec 14 18:45:51 2008 +0100
     9.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Dec 15 18:12:52 2008 +0100
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      HOL/Real/HahnBanach/Subspace.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Gertrud Bauer, TU Munich
     9.7  *)
     9.8  
     9.9 @@ -17,8 +16,8 @@
    9.10    and scalar multiplication.
    9.11  *}
    9.12  
    9.13 -locale subspace = var U + var V +
    9.14 -  constrains U :: "'a\<Colon>{minus, plus, zero, uminus} set"
    9.15 +locale subspace =
    9.16 +  fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and V
    9.17    assumes non_empty [iff, intro]: "U \<noteq> {}"
    9.18      and subset [iff]: "U \<subseteq> V"
    9.19      and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
    9.20 @@ -46,7 +45,7 @@
    9.21    assumes x: "x \<in> U" and y: "y \<in> U"
    9.22    shows "x - y \<in> U"
    9.23  proof -
    9.24 -  interpret vectorspace [V] by fact
    9.25 +  interpret vectorspace V by fact
    9.26    from x y show ?thesis by (simp add: diff_eq1 negate_eq1)
    9.27  qed
    9.28  
    9.29 @@ -60,11 +59,11 @@
    9.30    assumes "vectorspace V"
    9.31    shows "0 \<in> U"
    9.32  proof -
    9.33 -  interpret vectorspace [V] by fact
    9.34 -  have "U \<noteq> {}" by (rule U_V.non_empty)
    9.35 +  interpret V!: vectorspace V by fact
    9.36 +  have "U \<noteq> {}" by (rule non_empty)
    9.37    then obtain x where x: "x \<in> U" by blast
    9.38    then have "x \<in> V" .. then have "0 = x - x" by simp
    9.39 -  also from `vectorspace V` x x have "\<dots> \<in> U" by (rule U_V.diff_closed)
    9.40 +  also from `vectorspace V` x x have "\<dots> \<in> U" by (rule diff_closed)
    9.41    finally show ?thesis .
    9.42  qed
    9.43  
    9.44 @@ -73,7 +72,7 @@
    9.45    assumes x: "x \<in> U"
    9.46    shows "- x \<in> U"
    9.47  proof -
    9.48 -  interpret vectorspace [V] by fact
    9.49 +  interpret vectorspace V by fact
    9.50    from x show ?thesis by (simp add: negate_eq1)
    9.51  qed
    9.52  
    9.53 @@ -83,7 +82,7 @@
    9.54    assumes "vectorspace V"
    9.55    shows "vectorspace U"
    9.56  proof -
    9.57 -  interpret vectorspace [V] by fact
    9.58 +  interpret vectorspace V by fact
    9.59    show ?thesis
    9.60    proof
    9.61      show "U \<noteq> {}" ..
    9.62 @@ -255,8 +254,8 @@
    9.63    assumes "vectorspace U" "vectorspace V"
    9.64    shows "U \<unlhd> U + V"
    9.65  proof -
    9.66 -  interpret vectorspace [U] by fact
    9.67 -  interpret vectorspace [V] by fact
    9.68 +  interpret vectorspace U by fact
    9.69 +  interpret vectorspace V by fact
    9.70    show ?thesis
    9.71    proof
    9.72      show "U \<noteq> {}" ..
    9.73 @@ -279,9 +278,9 @@
    9.74    assumes "subspace U E" "vectorspace E" "subspace V E"
    9.75    shows "U + V \<unlhd> E"
    9.76  proof -
    9.77 -  interpret subspace [U E] by fact
    9.78 -  interpret vectorspace [E] by fact
    9.79 -  interpret subspace [V E] by fact
    9.80 +  interpret subspace U E by fact
    9.81 +  interpret vectorspace E by fact
    9.82 +  interpret subspace V E by fact
    9.83    show ?thesis
    9.84    proof
    9.85      have "0 \<in> U + V"
    9.86 @@ -346,9 +345,9 @@
    9.87      and sum: "u1 + v1 = u2 + v2"
    9.88    shows "u1 = u2 \<and> v1 = v2"
    9.89  proof -
    9.90 -  interpret vectorspace [E] by fact
    9.91 -  interpret subspace [U E] by fact
    9.92 -  interpret subspace [V E] by fact
    9.93 +  interpret vectorspace E by fact
    9.94 +  interpret subspace U E by fact
    9.95 +  interpret subspace V E by fact
    9.96    show ?thesis
    9.97    proof
    9.98      have U: "vectorspace U"  (* FIXME: use interpret *)
    9.99 @@ -395,8 +394,8 @@
   9.100      and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
   9.101    shows "y1 = y2 \<and> a1 = a2"
   9.102  proof -
   9.103 -  interpret vectorspace [E] by fact
   9.104 -  interpret subspace [H E] by fact
   9.105 +  interpret vectorspace E by fact
   9.106 +  interpret subspace H E by fact
   9.107    show ?thesis
   9.108    proof
   9.109      have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
   9.110 @@ -451,8 +450,8 @@
   9.111      and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   9.112    shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
   9.113  proof -
   9.114 -  interpret vectorspace [E] by fact
   9.115 -  interpret subspace [H E] by fact
   9.116 +  interpret vectorspace E by fact
   9.117 +  interpret subspace H E by fact
   9.118    show ?thesis
   9.119    proof (rule, simp_all only: split_paired_all split_conv)
   9.120      from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
   9.121 @@ -483,8 +482,8 @@
   9.122      and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   9.123    shows "h' x = h y + a * xi"
   9.124  proof -
   9.125 -  interpret vectorspace [E] by fact
   9.126 -  interpret subspace [H E] by fact
   9.127 +  interpret vectorspace E by fact
   9.128 +  interpret subspace H E by fact
   9.129    from x y x' have "x \<in> H + lin x'" by auto
   9.130    have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
   9.131    proof (rule ex_ex1I)
    10.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Sun Dec 14 18:45:51 2008 +0100
    10.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Dec 15 18:12:52 2008 +0100
    10.3 @@ -39,7 +39,9 @@
    10.4    the neutral element of scalar multiplication.
    10.5  *}
    10.6  
    10.7 -locale vectorspace = var V +
    10.8 +locale var_V = fixes V
    10.9 +
   10.10 +locale vectorspace = var_V +
   10.11    assumes non_empty [iff, intro?]: "V \<noteq> {}"
   10.12      and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
   10.13      and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
    11.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Sun Dec 14 18:45:51 2008 +0100
    11.2 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Mon Dec 15 18:12:52 2008 +0100
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      HOL/Real/HahnBanach/ZornLemma.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Gertrud Bauer, TU Munich
    11.7  *)
    11.8  
    12.1 --- a/src/HOL/Word/TdThs.thy	Sun Dec 14 18:45:51 2008 +0100
    12.2 +++ b/src/HOL/Word/TdThs.thy	Mon Dec 15 18:12:52 2008 +0100
    12.3 @@ -90,7 +90,7 @@
    12.4  
    12.5  end
    12.6  
    12.7 -interpretation nat_int: type_definition [int nat "Collect (op <= 0)"]
    12.8 +interpretation nat_int!: type_definition int nat "Collect (op <= 0)"
    12.9    by (rule td_nat_int)
   12.10  
   12.11  declare
    13.1 --- a/src/HOL/Word/WordDefinition.thy	Sun Dec 14 18:45:51 2008 +0100
    13.2 +++ b/src/HOL/Word/WordDefinition.thy	Mon Dec 15 18:12:52 2008 +0100
    13.3 @@ -356,11 +356,11 @@
    13.4  
    13.5  lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
    13.6  
    13.7 -interpretation word_uint: 
    13.8 -  td_ext ["uint::'a::len0 word \<Rightarrow> int" 
    13.9 -          word_of_int 
   13.10 -          "uints (len_of TYPE('a::len0))"
   13.11 -          "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"]
   13.12 +interpretation word_uint!:
   13.13 +  td_ext "uint::'a::len0 word \<Rightarrow> int" 
   13.14 +         word_of_int 
   13.15 +         "uints (len_of TYPE('a::len0))"
   13.16 +         "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
   13.17    by (rule td_ext_uint)
   13.18    
   13.19  lemmas td_uint = word_uint.td_thm
   13.20 @@ -368,11 +368,11 @@
   13.21  lemmas td_ext_ubin = td_ext_uint 
   13.22    [simplified len_gt_0 no_bintr_alt1 [symmetric]]
   13.23  
   13.24 -interpretation word_ubin:
   13.25 -  td_ext ["uint::'a::len0 word \<Rightarrow> int" 
   13.26 -          word_of_int 
   13.27 -          "uints (len_of TYPE('a::len0))"
   13.28 -          "bintrunc (len_of TYPE('a::len0))"]
   13.29 +interpretation word_ubin!:
   13.30 +  td_ext "uint::'a::len0 word \<Rightarrow> int" 
   13.31 +         word_of_int 
   13.32 +         "uints (len_of TYPE('a::len0))"
   13.33 +         "bintrunc (len_of TYPE('a::len0))"
   13.34    by (rule td_ext_ubin)
   13.35  
   13.36  lemma sint_sbintrunc': 
    14.1 --- a/src/HOL/ex/Abstract_NAT.thy	Sun Dec 14 18:45:51 2008 +0100
    14.2 +++ b/src/HOL/ex/Abstract_NAT.thy	Mon Dec 15 18:12:52 2008 +0100
    14.3 @@ -1,5 +1,4 @@
    14.4  (*
    14.5 -    ID:         $Id$
    14.6      Author:     Makarius
    14.7  *)
    14.8  
    14.9 @@ -131,7 +130,7 @@
   14.10  
   14.11  text {* \medskip Just see that our abstract specification makes sense \dots *}
   14.12  
   14.13 -interpretation NAT [0 Suc]
   14.14 +interpretation NAT 0 Suc
   14.15  proof (rule NAT.intro)
   14.16    fix m n
   14.17    show "(Suc m = Suc n) = (m = n)" by simp
    15.1 --- a/src/HOL/ex/Tarski.thy	Sun Dec 14 18:45:51 2008 +0100
    15.2 +++ b/src/HOL/ex/Tarski.thy	Mon Dec 15 18:12:52 2008 +0100
    15.3 @@ -120,7 +120,7 @@
    15.4  locale CL = S +
    15.5    assumes cl_co:  "cl : CompleteLattice"
    15.6  
    15.7 -interpretation CL < PO
    15.8 +sublocale CL < PO
    15.9  apply (simp_all add: A_def r_def)
   15.10  apply unfold_locales
   15.11  using cl_co unfolding CompleteLattice_def by auto
   15.12 @@ -131,7 +131,7 @@
   15.13    assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
   15.14    defines P_def: "P == fix f A"
   15.15  
   15.16 -interpretation CLF < CL
   15.17 +sublocale CLF < CL
   15.18  apply (simp_all add: A_def r_def)
   15.19  apply unfold_locales
   15.20  using f_cl unfolding CLF_set_def by auto
    16.1 --- a/src/HOL/plain.ML	Sun Dec 14 18:45:51 2008 +0100
    16.2 +++ b/src/HOL/plain.ML	Mon Dec 15 18:12:52 2008 +0100
    16.3 @@ -1,7 +1,7 @@
    16.4  (*  Title:      HOL/plain.ML
    16.5 -    ID:         $Id$
    16.6   
    16.7  Classical Higher-order Logic -- plain Tool bootstrap.
    16.8  *)
    16.9  
   16.10 +set new_locales;
   16.11  use_thy "Plain";