src/ZF/Constructible/Reflection.thy

 @{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) <-> Q(a,<y,z>)"}, removing most
 uses of @{term Pair_in_Mset}.  But there isn't much point in doing so, since 
 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)"
       and Pair_in_Mset : "[| x \<in> Mset(a); y \<in> Mset(a); Limit(a) |] 
                           ==> <x,y> \<in> Mset(a)"

 done
 
 
 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"
   assumes Cl_reflects: "[| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x)"
 

                    \<lambda>x. \<exists>z. M(z) \<and> P0(<x,z>), 
                    \<lambda>a x. \<exists>z\<in>Mset(a). Q0(a,<x,z>))" 
 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
 
 lemma (in reflection) All_reflection_0:
      "Reflects(Cl,P0,Q0)