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/Datatype_absolute.thy
changeset 13382 b37764a46b16
parent 13363 c26eeb000470
child 13385 31df66ca0780 
--- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 16 18:46:13 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 16 18:46:59 2002 +0200
@@ -154,7 +154,7 @@
 by (simp add: is_list_functor_def singleton_0 nat_into_M)
 
 
-locale M_datatypes = M_wfrank +
+locale (open) M_datatypes = M_wfrank +
  assumes list_replacement1: 
    "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
   and list_replacement2:
isabelle