src/ZF/Constructible/Datatype_absolute.thy
changeset 13428 99e52e78eb65
parent 13423 7ec771711c09
child 13440 cdde97e1db1c
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Sun Jul 28 21:09:37 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Mon Jul 29 00:57:16 2002 +0200
     1.3 @@ -362,7 +362,7 @@
     1.4    is_formula :: "[i=>o,i] => o"
     1.5      "is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
     1.6  
     1.7 -locale (open) M_datatypes = M_wfrank +
     1.8 +locale M_datatypes = M_wfrank +
     1.9   assumes list_replacement1: 
    1.10     "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    1.11    and list_replacement2: 
    1.12 @@ -506,7 +506,7 @@
    1.13      "is_eclose(M,A,Z) == \<forall>u[M]. u \<in> Z <-> mem_eclose(M,A,u)"
    1.14  
    1.15  
    1.16 -locale (open) M_eclose = M_datatypes +
    1.17 +locale M_eclose = M_datatypes +
    1.18   assumes eclose_replacement1: 
    1.19     "M(A) ==> iterates_replacement(M, big_union(M), A)"
    1.20    and eclose_replacement2: