src/ZF/Constructible/Reflection.thy
2015-12-30 wenzelm 2015-12-30 clarified syntax;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-11-01 wenzelm 2014-11-01 eliminated spurious semicolons;
2012-03-06 paulson 2012-03-06 More mathematical symbols for ZF examples
2010-04-23 wenzelm 2010-04-23 mark schematic statements explicitly;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2006-11-07 wenzelm 2006-11-07 fixed locale fact references;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2002-10-09 paulson 2002-10-09 Re-organization of Constructible theories
2002-09-10 paulson 2002-09-10 tweaks
2002-08-16 paulson 2002-08-16 Relativized right up to L satisfies V=L!
2002-07-30 paulson 2002-07-30 better sats rules for higher-order operators
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-04 paulson 2002-07-04 reflection for rall and rex
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