# HG changeset patch
# User ballarin
# Date 1229361172 -3600
# Node ID 60f7fb56f8cd64081be199e5aa098d6d68a294f3
# Parent  ce6d35a0bed644fce70241b11ddc7a2df0f063e6
More porting to new locales.

diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/NSA/StarDef.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -23,7 +23,7 @@
 apply (rule nat_infinite)
 done
 
-interpretation FreeUltrafilterNat: freeultrafilter [FreeUltrafilterNat]
+interpretation FreeUltrafilterNat!: freeultrafilter FreeUltrafilterNat
 by (rule freeultrafilter_FreeUltrafilterNat)
 
 text {* This rule takes the place of the old ultra tactic *}
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/Bounds.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -27,7 +26,7 @@
   assumes "lub A x"
   shows "\<Squnion>A = (x::'a::order)"
 proof -
-  interpret lub [A x] by fact
+  interpret lub A x by fact
   show ?thesis
   proof (unfold the_lub_def)
     from `lub A x` show "The (lub A) = x"
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/FunctionNorm.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -22,7 +21,7 @@
   linear forms:
 *}
 
-locale continuous = var V + norm_syntax + linearform +
+locale continuous = var_V + norm_syntax + linearform +
   assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
 
 declare continuous.intro [intro?] continuous_axioms.intro [intro?]
@@ -91,7 +90,7 @@
   assumes "continuous V norm f"
   shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
 proof -
-  interpret continuous [V norm f] by fact
+  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. *}
@@ -159,7 +158,7 @@
   assumes b: "b \<in> B V f"
   shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
-  interpret continuous [V norm f] by fact
+  interpret continuous V norm f by fact
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
     using `continuous V norm f` by (rule fn_norm_works)
   from this and b show ?thesis ..
@@ -170,7 +169,7 @@
   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
+  interpret continuous V norm f by fact
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
     using `continuous V norm f` by (rule fn_norm_works)
   from this and b show ?thesis ..
@@ -182,7 +181,7 @@
   assumes "continuous V norm f"
   shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
-  interpret continuous [V norm f] by fact
+  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. *}
@@ -204,8 +203,8 @@
   assumes x: "x \<in> V"
   shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
 proof -
-  interpret continuous [V norm f] by fact
-  interpret linearform [V f] .
+  interpret continuous V norm f by fact
+  interpret linearform V f .
   show ?thesis
   proof cases
     assume "x = 0"
@@ -246,7 +245,7 @@
   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 -
-  interpret continuous [V norm f] by fact
+  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"
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -63,10 +62,10 @@
     -- {* 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
+  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"
   then have M: "M = \<dots>" by (simp only:)
   from E have F: "vectorspace F" ..
@@ -322,10 +321,10 @@
     \<and> (\<forall>x \<in> F. g x = f x)
     \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
 proof -
-  interpret vectorspace [E] by fact
-  interpret subspace [F E] by fact
-  interpret linearform [F f] by fact
-  interpret seminorm [E p] by fact
+  interpret vectorspace E by fact
+  interpret subspace F E by fact
+  interpret linearform F f by fact
+  interpret seminorm E p by fact
   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)
@@ -363,12 +362,12 @@
      \<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]
+  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
+  interpret subspace F E by fact
+  interpret linearform F f by fact
+  interpret continuous F norm f by fact
   have E: "vectorspace E" by intro_locales
   have F: "vectorspace F" by rule intro_locales
   have F_norm: "normed_vectorspace F norm"
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -46,7 +45,7 @@
   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
+  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. *}
@@ -98,8 +97,8 @@
   assumes E: "vectorspace E"
   shows "linearform H' h'"
 proof -
-  interpret linearform [H h] by fact
-  interpret vectorspace [E] by fact
+  interpret linearform H h by fact
+  interpret vectorspace E by fact
   show ?thesis
   proof
     note E = `vectorspace E`
@@ -203,10 +202,10 @@
     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 -
-  interpret vectorspace [E] by fact
-  interpret subspace [H E] by fact
-  interpret seminorm [E p] by fact
-  interpret linearform [H h] by fact
+  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'"
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -405,10 +405,10 @@
     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
+  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 ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/Linearform.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -14,8 +13,8 @@
   that is additive and multiplicative.
 *}
 
-locale linearform = var V + var f +
-  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
+locale linearform =
+  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f
   assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
     and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
 
@@ -25,7 +24,7 @@
   assumes "vectorspace V"
   shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   assume x: "x \<in> V"
   then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
   also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
@@ -37,7 +36,7 @@
   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
+  interpret vectorspace V by fact
   assume x: "x \<in> V" and y: "y \<in> V"
   then have "x - y = x + - y" by (rule diff_eq1)
   also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
@@ -51,7 +50,7 @@
   assumes "vectorspace V"
   shows "f 0 = 0"
 proof -
-  interpret vectorspace [V] by fact
+  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 ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/NormedSpace.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -20,7 +19,7 @@
 locale norm_syntax =
   fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
 
-locale seminorm = var V + norm_syntax +
+locale seminorm = var_V + norm_syntax +
   constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
   assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
     and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
@@ -32,7 +31,7 @@
   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
+  interpret vectorspace V by fact
   assume x: "x \<in> V" and y: "y \<in> V"
   then have "x - y = x + - 1 \<cdot> y"
     by (simp add: diff_eq2 negate_eq2a)
@@ -48,7 +47,7 @@
   assumes "vectorspace V"
   shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   assume x: "x \<in> V"
   then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
   also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
@@ -103,8 +102,8 @@
   assumes "subspace F E" "normed_vectorspace E norm"
   shows "normed_vectorspace F norm"
 proof -
-  interpret subspace [F E] by fact
-  interpret normed_vectorspace [E norm] by fact
+  interpret subspace F E by fact
+  interpret normed_vectorspace E norm by fact
   show ?thesis
   proof
     show "vectorspace F" by (rule vectorspace) unfold_locales
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/Subspace.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
@@ -17,8 +16,8 @@
   and scalar multiplication.
 *}
 
-locale subspace = var U + var V +
-  constrains U :: "'a\<Colon>{minus, plus, zero, uminus} set"
+locale subspace =
+  fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and V
   assumes non_empty [iff, intro]: "U \<noteq> {}"
     and subset [iff]: "U \<subseteq> V"
     and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
@@ -46,7 +45,7 @@
   assumes x: "x \<in> U" and y: "y \<in> U"
   shows "x - y \<in> U"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   from x y show ?thesis by (simp add: diff_eq1 negate_eq1)
 qed
 
@@ -60,11 +59,11 @@
   assumes "vectorspace V"
   shows "0 \<in> U"
 proof -
-  interpret vectorspace [V] by fact
-  have "U \<noteq> {}" by (rule U_V.non_empty)
+  interpret V!: vectorspace V by fact
+  have "U \<noteq> {}" by (rule non_empty)
   then obtain x where x: "x \<in> U" by blast
   then have "x \<in> V" .. then have "0 = x - x" by simp
-  also from `vectorspace V` x x have "\<dots> \<in> U" by (rule U_V.diff_closed)
+  also from `vectorspace V` x x have "\<dots> \<in> U" by (rule diff_closed)
   finally show ?thesis .
 qed
 
@@ -73,7 +72,7 @@
   assumes x: "x \<in> U"
   shows "- x \<in> U"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   from x show ?thesis by (simp add: negate_eq1)
 qed
 
@@ -83,7 +82,7 @@
   assumes "vectorspace V"
   shows "vectorspace U"
 proof -
-  interpret vectorspace [V] by fact
+  interpret vectorspace V by fact
   show ?thesis
   proof
     show "U \<noteq> {}" ..
@@ -255,8 +254,8 @@
   assumes "vectorspace U" "vectorspace V"
   shows "U \<unlhd> U + V"
 proof -
-  interpret vectorspace [U] by fact
-  interpret vectorspace [V] by fact
+  interpret vectorspace U by fact
+  interpret vectorspace V by fact
   show ?thesis
   proof
     show "U \<noteq> {}" ..
@@ -279,9 +278,9 @@
   assumes "subspace U E" "vectorspace E" "subspace V E"
   shows "U + V \<unlhd> E"
 proof -
-  interpret subspace [U E] by fact
-  interpret vectorspace [E] by fact
-  interpret subspace [V E] by fact
+  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"
@@ -346,9 +345,9 @@
     and sum: "u1 + v1 = u2 + v2"
   shows "u1 = u2 \<and> v1 = v2"
 proof -
-  interpret vectorspace [E] by fact
-  interpret subspace [U E] by fact
-  interpret subspace [V E] by fact
+  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 *)
@@ -395,8 +394,8 @@
     and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
   shows "y1 = y2 \<and> a1 = a2"
 proof -
-  interpret vectorspace [E] by fact
-  interpret subspace [H E] by fact
+  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'"
@@ -451,8 +450,8 @@
     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 -
-  interpret vectorspace [E] by fact
-  interpret subspace [H E] by fact
+  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
@@ -483,8 +482,8 @@
     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
+  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)
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -39,7 +39,9 @@
   the neutral element of scalar multiplication.
 *}
 
-locale vectorspace = var V +
+locale var_V = fixes V
+
+locale vectorspace = var_V +
   assumes non_empty [iff, intro?]: "V \<noteq> {}"
     and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
     and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Real/HahnBanach/ZornLemma.thy
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/HahnBanach/ZornLemma.thy
-    ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 *)
 
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Word/TdThs.thy
--- a/src/HOL/Word/TdThs.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Word/TdThs.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -90,7 +90,7 @@
 
 end
 
-interpretation nat_int: type_definition [int nat "Collect (op <= 0)"]
+interpretation nat_int!: type_definition int nat "Collect (op <= 0)"
   by (rule td_nat_int)
 
 declare
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Word/WordDefinition.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -356,11 +356,11 @@
 
 lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
 
-interpretation word_uint: 
-  td_ext ["uint::'a::len0 word \<Rightarrow> int" 
-          word_of_int 
-          "uints (len_of TYPE('a::len0))"
-          "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"]
+interpretation word_uint!:
+  td_ext "uint::'a::len0 word \<Rightarrow> int" 
+         word_of_int 
+         "uints (len_of TYPE('a::len0))"
+         "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
   by (rule td_ext_uint)
   
 lemmas td_uint = word_uint.td_thm
@@ -368,11 +368,11 @@
 lemmas td_ext_ubin = td_ext_uint 
   [simplified len_gt_0 no_bintr_alt1 [symmetric]]
 
-interpretation word_ubin:
-  td_ext ["uint::'a::len0 word \<Rightarrow> int" 
-          word_of_int 
-          "uints (len_of TYPE('a::len0))"
-          "bintrunc (len_of TYPE('a::len0))"]
+interpretation word_ubin!:
+  td_ext "uint::'a::len0 word \<Rightarrow> int" 
+         word_of_int 
+         "uints (len_of TYPE('a::len0))"
+         "bintrunc (len_of TYPE('a::len0))"
   by (rule td_ext_ubin)
 
 lemma sint_sbintrunc': 
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/ex/Abstract_NAT.thy
--- a/src/HOL/ex/Abstract_NAT.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/ex/Abstract_NAT.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -1,5 +1,4 @@
 (*
-    ID:         $Id$
     Author:     Makarius
 *)
 
@@ -131,7 +130,7 @@
 
 text {* \medskip Just see that our abstract specification makes sense \dots *}
 
-interpretation NAT [0 Suc]
+interpretation NAT 0 Suc
 proof (rule NAT.intro)
   fix m n
   show "(Suc m = Suc n) = (m = n)" by simp
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/ex/Tarski.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -120,7 +120,7 @@
 locale CL = S +
   assumes cl_co:  "cl : CompleteLattice"
 
-interpretation CL < PO
+sublocale CL < PO
 apply (simp_all add: A_def r_def)
 apply unfold_locales
 using cl_co unfolding CompleteLattice_def by auto
@@ -131,7 +131,7 @@
   assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
   defines P_def: "P == fix f A"
 
-interpretation CLF < CL
+sublocale CLF < CL
 apply (simp_all add: A_def r_def)
 apply unfold_locales
 using f_cl unfolding CLF_set_def by auto
diff -r ce6d35a0bed6 -r 60f7fb56f8cd src/HOL/plain.ML
--- a/src/HOL/plain.ML	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/plain.ML	Mon Dec 15 18:12:52 2008 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/plain.ML
-    ID:         $Id$
  
 Classical Higher-order Logic -- plain Tool bootstrap.
 *)
 
+set new_locales;
 use_thy "Plain";