--- a/src/ZF/AC/AC16_WO4.thy Tue Jul 16 18:46:13 2002 +0200
+++ b/src/ZF/AC/AC16_WO4.thy Tue Jul 16 18:46:59 2002 +0200
@@ -203,7 +203,7 @@
succ_lepoll_natE)
-locale AC16 =
+locale (open) AC16 =
fixes x and y and k and l and m and t_n and R and MM and LL and GG and s
defines k_def: "k == succ(l)"
and MM_def: "MM == {v \<in> t_n. succ(k) \<lesssim> v Int y}"
--- a/src/ZF/AC/DC.thy Tue Jul 16 18:46:13 2002 +0200
+++ b/src/ZF/AC/DC.thy Tue Jul 16 18:46:59 2002 +0200
@@ -94,7 +94,7 @@
transrec(b, %c r. THE x. first(x, {x \<in> X. <r``c, x> \<in> R}, Q))"
-locale DC0_imp =
+locale (open) DC0_imp =
fixes XX and RR and X and R
assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat --> (\<exists>x \<in> X. <Y, x> \<in> R)"
@@ -292,7 +292,7 @@
done
-locale imp_DC0 =
+locale (open) imp_DC0 =
fixes XX and RR and x and R and f and allRR
defines XX_def: "XX == (\<Union>n \<in> nat.
{f \<in> succ(n)->domain(R). \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})"
--- a/src/ZF/Constructible/Datatype_absolute.thy Tue Jul 16 18:46:13 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Tue Jul 16 18:46:59 2002 +0200
@@ -154,7 +154,7 @@
by (simp add: is_list_functor_def singleton_0 nat_into_M)
-locale M_datatypes = M_wfrank +
+locale (open) M_datatypes = M_wfrank +
assumes list_replacement1:
"M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
and list_replacement2:
--- a/src/ZF/Constructible/Normal.thy Tue Jul 16 18:46:13 2002 +0200
+++ b/src/ZF/Constructible/Normal.thy Tue Jul 16 18:46:59 2002 +0200
@@ -72,7 +72,7 @@
c.u.*}
text{*The constructions below come from Kunen, \emph{Set Theory}, page 78.*}
-locale cub_family =
+locale (open) cub_family =
fixes P and A
fixes next_greater -- "the next ordinal satisfying class @{term A}"
fixes sup_greater -- "sup of those ordinals over all @{term A}"
--- a/src/ZF/Constructible/Reflection.thy Tue Jul 16 18:46:13 2002 +0200
+++ b/src/ZF/Constructible/Reflection.thy Tue Jul 16 18:46:59 2002 +0200
@@ -25,7 +25,7 @@
ultimately the @{text ex_reflection} proof is packaged up using the
predicate @{text Reflects}.
*}
-locale reflection =
+locale (open) reflection =
fixes Mset and M and Reflects
assumes Mset_mono_le : "mono_le_subset(Mset)"
and Mset_cont : "cont_Ord(Mset)"
@@ -124,7 +124,7 @@
text{*Locale for the induction hypothesis*}
-locale ex_reflection = reflection +
+locale (open) ex_reflection = reflection +
fixes P --"the original formula"
fixes Q --"the reflected formula"
fixes Cl --"the class of reflecting ordinals"
@@ -192,7 +192,7 @@
apply (simp add: Reflects_def)
apply (intro conjI Closed_Unbounded_Int)
apply blast
- apply (rule reflection.Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify)
+ apply (rule Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify)
apply (rule_tac Cl=Cl in ClEx_iff, assumption+, blast)
done
--- a/src/ZF/Constructible/Relative.thy Tue Jul 16 18:46:13 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Tue Jul 16 18:46:59 2002 +0200
@@ -410,7 +410,7 @@
text{*The class M is assumed to be transitive and to satisfy some
relativized ZF axioms*}
-locale M_triv_axioms =
+locale (open) M_triv_axioms =
fixes M
assumes transM: "[| y\<in>x; M(x) |] ==> M(y)"
and nonempty [simp]: "M(0)"
@@ -780,7 +780,7 @@
subsection{*Some instances of separation and strong replacement*}
-locale M_axioms = M_triv_axioms +
+locale (open) M_axioms = M_triv_axioms +
assumes Inter_separation:
"M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
and cartprod_separation:
--- a/src/ZF/Constructible/WF_absolute.thy Tue Jul 16 18:46:13 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Tue Jul 16 18:46:59 2002 +0200
@@ -143,7 +143,7 @@
by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD])
-locale M_trancl = M_axioms +
+locale (open) M_trancl = M_axioms +
assumes rtrancl_separation:
"[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
and wellfounded_trancl_separation:
@@ -231,7 +231,7 @@
rank function.*}
-locale M_wfrank = M_trancl +
+locale (open) M_wfrank = M_trancl +
assumes wfrank_separation:
"M(r) ==>
separation (M, \<lambda>x.
--- a/src/ZF/Constructible/WFrec.thy Tue Jul 16 18:46:13 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Tue Jul 16 18:46:59 2002 +0200
@@ -378,7 +378,7 @@
fun_apply(M,f,j,fj) & fj = k"
-locale M_ord_arith = M_axioms +
+locale (open) M_ord_arith = M_axioms +
assumes oadd_strong_replacement:
"[| M(i); M(j) |] ==>
strong_replacement(M,