src/ZF/Constructible/Rec_Separation.thy
changeset 13647 7f6f0ffc45c3
parent 13634 99a593b49b04
child 13651 ac80e101306a
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Mon Oct 14 10:44:32 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Oct 14 11:32:00 2002 +0200
     1.3 @@ -204,22 +204,9 @@
     1.4  
     1.5  lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
     1.6    and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
     1.7 -  and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L]
     1.8 -  and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L]
     1.9 -  and trancl_closed = M_trancl.trancl_closed [OF M_trancl_L]
    1.10 -  and trancl_abs = M_trancl.trancl_abs [OF M_trancl_L]
    1.11 -  and wellfounded_on_trancl = M_trancl.wellfounded_on_trancl [OF M_trancl_L]
    1.12 -  and wellfounded_trancl = M_trancl.wellfounded_trancl [OF M_trancl_L]
    1.13 -  and wfrec_relativize = M_trancl.wfrec_relativize [OF M_trancl_L]
    1.14 -  and trans_wfrec_relativize = M_trancl.trans_wfrec_relativize [OF M_trancl_L]
    1.15    and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L]
    1.16 -  and trans_eq_pair_wfrec_iff = M_trancl.trans_eq_pair_wfrec_iff [OF M_trancl_L]
    1.17    and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L]
    1.18  
    1.19 -declare rtrancl_closed [intro,simp]
    1.20 -declare rtrancl_abs [simp]
    1.21 -declare trancl_closed [intro,simp]
    1.22 -declare trancl_abs [simp]
    1.23  
    1.24  
    1.25  subsection{*@{term L} is Closed Under the Operator @{term list}*}