src/ZF/Constructible/WF_absolute.thy
changeset 13428 99e52e78eb65
parent 13418 7c0ba9dba978
child 13505 52a16cb7fefb
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Sun Jul 28 21:09:37 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Mon Jul 29 00:57:16 2002 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4  by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD]) 
     1.5  
     1.6  
     1.7 -locale (open) M_trancl = M_axioms +
     1.8 +locale M_trancl = M_axioms +
     1.9    assumes rtrancl_separation:
    1.10  	 "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
    1.11        and wellfounded_trancl_separation:
    1.12 @@ -231,7 +231,7 @@
    1.13  rank function.*}
    1.14  
    1.15  
    1.16 -locale (open) M_wfrank = M_trancl +
    1.17 +locale M_wfrank = M_trancl +
    1.18    assumes wfrank_separation:
    1.19       "M(r) ==>
    1.20        separation (M, \<lambda>x. 
    1.21 @@ -317,7 +317,7 @@
    1.22      "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
    1.23       ==> \<forall>f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
    1.24  apply (drule wellfounded_trancl, assumption)
    1.25 -apply (rule wellfounded_induct, assumption+)
    1.26 +apply (rule wellfounded_induct, assumption, erule (1) transM)
    1.27    apply simp
    1.28   apply (blast intro: Ord_wfrank_separation', clarify)
    1.29  txt{*The reasoning in both cases is that we get @{term y} such that
    1.30 @@ -445,7 +445,8 @@
    1.31  apply (subgoal_tac "a\<in>A & b\<in>A")
    1.32   prefer 2 apply blast
    1.33  apply (simp add: lt_def Ord_wellfoundedrank, clarify)
    1.34 -apply (frule exists_wfrank [of concl: _ b], assumption+, clarify)
    1.35 +apply (frule exists_wfrank [of concl: _ b], erule (1) transM, assumption)
    1.36 +apply clarify
    1.37  apply (rename_tac fb)
    1.38  apply (frule is_recfun_restrict [of concl: "r^+" a])
    1.39      apply (rule trans_trancl, assumption)