src/ZF/Constructible/Rec_Separation.thy
changeset 13564 1500a2e48d44
parent 13506 acc18a5d2b1a
child 13566 52a419210d5c
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Sep 10 16:47:17 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Sep 10 16:51:31 2002 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4  
     1.5  theorem M_trancl_L: "PROP M_trancl(L)"
     1.6  by (rule M_trancl.intro
     1.7 -         [OF M_triv_axioms_L M_axioms_axioms_L M_trancl_axioms_L])
     1.8 +         [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L])
     1.9  
    1.10  lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
    1.11    and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]