src/ZF/Constructible/Normal.thy
2002-07-29 wenzelm 2002-07-29 eliminate open locales and special ML code;
2002-07-16 wenzelm 2002-07-16 adapted locales;
2002-07-01 paulson 2002-07-01 more use of relativized quantifiers list_closed
2002-06-19 paulson 2002-06-19 new theory of inner models