More porting to new locales.
--- 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 *}
--- 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"
--- 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"
--- 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"
--- 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'"
--- 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
--- 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
--- 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
--- 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)
--- 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"
--- 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
*)
--- 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
--- 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':
--- 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
--- 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
--- 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";