# HG changeset patch
# User wenzelm
# Date 1026838019 -7200
# Node ID b37764a46b16990ad77cd79d7182071adfea3e13
# Parent  60bc63b1385779e66bef1b1022c0d18feb37d5c5
adapted locales;

diff -r 60bc63b13857 -r b37764a46b16 src/ZF/AC/AC16_WO4.thy
--- 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}"
diff -r 60bc63b13857 -r b37764a46b16 src/ZF/AC/DC.thy
--- 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})"
diff -r 60bc63b13857 -r b37764a46b16 src/ZF/Constructible/Datatype_absolute.thy
--- 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: 
diff -r 60bc63b13857 -r b37764a46b16 src/ZF/Constructible/Normal.thy
--- 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}"
diff -r 60bc63b13857 -r b37764a46b16 src/ZF/Constructible/Reflection.thy
--- 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
 
diff -r 60bc63b13857 -r b37764a46b16 src/ZF/Constructible/Relative.thy
--- 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:
diff -r 60bc63b13857 -r b37764a46b16 src/ZF/Constructible/WF_absolute.thy
--- 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. 
diff -r 60bc63b13857 -r b37764a46b16 src/ZF/Constructible/WFrec.thy
--- 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,