adapted locales;
authorwenzelm
Tue Jul 16 18:46:59 2002 +0200 (2002-07-16)
changeset 13382b37764a46b16
parent 13381 60bc63b13857
child 13383 041d78bf9403
adapted locales;
src/ZF/AC/AC16_WO4.thy
src/ZF/AC/DC.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/Reflection.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
     1.1 --- a/src/ZF/AC/AC16_WO4.thy	Tue Jul 16 18:46:13 2002 +0200
     1.2 +++ b/src/ZF/AC/AC16_WO4.thy	Tue Jul 16 18:46:59 2002 +0200
     1.3 @@ -203,7 +203,7 @@
     1.4                   succ_lepoll_natE)
     1.5  
     1.6  
     1.7 -locale AC16 =
     1.8 +locale (open) AC16 =
     1.9    fixes x and y and k and l and m and t_n and R and MM and LL and GG and s 
    1.10    defines k_def:     "k   == succ(l)"
    1.11        and MM_def:    "MM  == {v \<in> t_n. succ(k) \<lesssim> v Int y}"
     2.1 --- a/src/ZF/AC/DC.thy	Tue Jul 16 18:46:13 2002 +0200
     2.2 +++ b/src/ZF/AC/DC.thy	Tue Jul 16 18:46:59 2002 +0200
     2.3 @@ -94,7 +94,7 @@
     2.4  	   transrec(b, %c r. THE x. first(x, {x \<in> X. <r``c, x> \<in> R}, Q))"
     2.5  
     2.6  
     2.7 -locale DC0_imp =
     2.8 +locale (open) DC0_imp =
     2.9    fixes XX and RR and X and R
    2.10  
    2.11    assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat --> (\<exists>x \<in> X. <Y, x> \<in> R)"
    2.12 @@ -292,7 +292,7 @@
    2.13  done
    2.14  
    2.15  
    2.16 -locale imp_DC0 =
    2.17 +locale (open) imp_DC0 =
    2.18    fixes XX and RR and x and R and f and allRR
    2.19    defines XX_def: "XX == (\<Union>n \<in> nat.
    2.20  		      {f \<in> succ(n)->domain(R). \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})"
     3.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 16 18:46:13 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 16 18:46:59 2002 +0200
     3.3 @@ -154,7 +154,7 @@
     3.4  by (simp add: is_list_functor_def singleton_0 nat_into_M)
     3.5  
     3.6  
     3.7 -locale M_datatypes = M_wfrank +
     3.8 +locale (open) M_datatypes = M_wfrank +
     3.9   assumes list_replacement1: 
    3.10     "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    3.11    and list_replacement2: 
     4.1 --- a/src/ZF/Constructible/Normal.thy	Tue Jul 16 18:46:13 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Normal.thy	Tue Jul 16 18:46:59 2002 +0200
     4.3 @@ -72,7 +72,7 @@
     4.4        c.u.*}
     4.5  
     4.6  text{*The constructions below come from Kunen, \emph{Set Theory}, page 78.*}
     4.7 -locale cub_family =
     4.8 +locale (open) cub_family =
     4.9    fixes P and A
    4.10    fixes next_greater -- "the next ordinal satisfying class @{term A}"
    4.11    fixes sup_greater  -- "sup of those ordinals over all @{term A}"
     5.1 --- a/src/ZF/Constructible/Reflection.thy	Tue Jul 16 18:46:13 2002 +0200
     5.2 +++ b/src/ZF/Constructible/Reflection.thy	Tue Jul 16 18:46:59 2002 +0200
     5.3 @@ -25,7 +25,7 @@
     5.4  ultimately the @{text ex_reflection} proof is packaged up using the
     5.5  predicate @{text Reflects}.
     5.6  *}
     5.7 -locale reflection =
     5.8 +locale (open) reflection =
     5.9    fixes Mset and M and Reflects
    5.10    assumes Mset_mono_le : "mono_le_subset(Mset)"
    5.11        and Mset_cont    : "cont_Ord(Mset)"
    5.12 @@ -124,7 +124,7 @@
    5.13  
    5.14  text{*Locale for the induction hypothesis*}
    5.15  
    5.16 -locale ex_reflection = reflection +
    5.17 +locale (open) ex_reflection = reflection +
    5.18    fixes P  --"the original formula"
    5.19    fixes Q  --"the reflected formula"
    5.20    fixes Cl --"the class of reflecting ordinals"
    5.21 @@ -192,7 +192,7 @@
    5.22  apply (simp add: Reflects_def) 
    5.23  apply (intro conjI Closed_Unbounded_Int)
    5.24    apply blast 
    5.25 - apply (rule reflection.Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify) 
    5.26 + apply (rule Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify) 
    5.27  apply (rule_tac Cl=Cl in  ClEx_iff, assumption+, blast) 
    5.28  done
    5.29  
     6.1 --- a/src/ZF/Constructible/Relative.thy	Tue Jul 16 18:46:13 2002 +0200
     6.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Jul 16 18:46:59 2002 +0200
     6.3 @@ -410,7 +410,7 @@
     6.4  
     6.5  text{*The class M is assumed to be transitive and to satisfy some
     6.6        relativized ZF axioms*}
     6.7 -locale M_triv_axioms =
     6.8 +locale (open) M_triv_axioms =
     6.9    fixes M
    6.10    assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
    6.11        and nonempty [simp]:  "M(0)"
    6.12 @@ -780,7 +780,7 @@
    6.13  
    6.14  subsection{*Some instances of separation and strong replacement*}
    6.15  
    6.16 -locale M_axioms = M_triv_axioms +
    6.17 +locale (open) M_axioms = M_triv_axioms +
    6.18  assumes Inter_separation:
    6.19       "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
    6.20    and cartprod_separation:
     7.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Jul 16 18:46:13 2002 +0200
     7.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Jul 16 18:46:59 2002 +0200
     7.3 @@ -143,7 +143,7 @@
     7.4  by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD]) 
     7.5  
     7.6  
     7.7 -locale M_trancl = M_axioms +
     7.8 +locale (open) M_trancl = M_axioms +
     7.9    assumes rtrancl_separation:
    7.10  	 "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
    7.11        and wellfounded_trancl_separation:
    7.12 @@ -231,7 +231,7 @@
    7.13  rank function.*}
    7.14  
    7.15  
    7.16 -locale M_wfrank = M_trancl +
    7.17 +locale (open) M_wfrank = M_trancl +
    7.18    assumes wfrank_separation:
    7.19       "M(r) ==>
    7.20        separation (M, \<lambda>x. 
     8.1 --- a/src/ZF/Constructible/WFrec.thy	Tue Jul 16 18:46:13 2002 +0200
     8.2 +++ b/src/ZF/Constructible/WFrec.thy	Tue Jul 16 18:46:59 2002 +0200
     8.3 @@ -378,7 +378,7 @@
     8.4                    fun_apply(M,f,j,fj) & fj = k"
     8.5  
     8.6  
     8.7 -locale M_ord_arith = M_axioms +
     8.8 +locale (open) M_ord_arith = M_axioms +
     8.9    assumes oadd_strong_replacement:
    8.10     "[| M(i); M(j) |] ==>
    8.11      strong_replacement(M,