src/ZF/Constructible/WF_absolute.thy
changeset 13564 1500a2e48d44
parent 13506 acc18a5d2b1a
child 13615 449a70d88b38
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Sep 10 16:47:17 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Sep 10 16:51:31 2002 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4      "tran_closure(M,r,t) ==
     1.5           \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)"
     1.6  
     1.7 -lemma (in M_axioms) rtran_closure_mem_iff:
     1.8 +lemma (in M_basic) rtran_closure_mem_iff:
     1.9       "[|M(A); M(r); M(p)|]
    1.10        ==> rtran_closure_mem(M,A,r,p) <->
    1.11            (\<exists>n[M]. n\<in>nat & 
    1.12 @@ -149,7 +149,7 @@
    1.13  by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD]) 
    1.14  
    1.15  
    1.16 -locale M_trancl = M_axioms +
    1.17 +locale M_trancl = M_basic +
    1.18    assumes rtrancl_separation:
    1.19  	 "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
    1.20        and wellfounded_trancl_separation: