src/ZF/Constructible/MetaExists.thy
2017-04-09 wenzelm 2017-04-09 clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
2015-10-10 wenzelm 2015-10-10 tuned syntax -- more symbols;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 tuned specifications;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2002-10-09 paulson 2002-10-09 Re-organization of Constructible theories
2002-08-16 paulson 2002-08-16 Relativized right up to L satisfies V=L!
2002-07-08 wenzelm 2002-07-08 tuned;
2002-07-08 paulson 2002-07-08 Defining a meta-existential quantifier. Using it to streamline reflection proofs.