src/ZF/Constructible/Relative.thy

 
 subsection{*Absoluteness for a transitive class model*}
 
 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)"
       and upair_ax:	    "upair_ax(M)"
       and Union_ax:	    "Union_ax(M)"

        "natnumber(M,0,x) == x=0"
 *)
 
 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:
      "[| M(A); M(B) |] 
       ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"