equal
deleted
inserted
replaced
210 apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+ |
210 apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+ |
211 done |
211 done |
212 |
212 |
213 theorem M_trancl_L: "PROP M_trancl(L)" |
213 theorem M_trancl_L: "PROP M_trancl(L)" |
214 by (rule M_trancl.intro |
214 by (rule M_trancl.intro |
215 [OF M_triv_axioms_L M_axioms_axioms_L M_trancl_axioms_L]) |
215 [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L]) |
216 |
216 |
217 lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L] |
217 lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L] |
218 and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L] |
218 and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L] |
219 and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L] |
219 and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L] |
220 and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L] |
220 and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L] |