Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Constructible/Rec_Separation.thy
changeset 13564 1500a2e48d44
parent 13506 acc18a5d2b1a
child 13566 52a419210d5c 
--- a/src/ZF/Constructible/Rec_Separation.thy	Tue Sep 10 16:47:17 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Sep 10 16:51:31 2002 +0200
@@ -212,7 +212,7 @@
 
 theorem M_trancl_L: "PROP M_trancl(L)"
 by (rule M_trancl.intro
-         [OF M_triv_axioms_L M_axioms_axioms_L M_trancl_axioms_L])
+         [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L])
 
 lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
   and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
isabelle