src/HOL/ZF/HOLZF.thy
2012-03-01 haftmann 2012-03-01 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2011-12-13 wenzelm 2011-12-13 modernized specifications;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-03-02 krauss 2010-03-02 removed obsolete helper theory
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-10-22 nipkow 2009-10-22 inv_onto -> inv_into
2009-10-18 nipkow 2009-10-18 merged
2009-10-18 nipkow 2009-10-18 Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts;
2007-09-30 wenzelm 2007-09-30 avoid unnamed infixes;
2007-08-02 wenzelm 2007-08-02 turned simp_depth_limit into configuration option;
2007-06-11 chaieb 2007-06-11 tuned Proof
2007-04-15 wenzelm 2007-04-15 replaced axioms/finalconsts by proper axiomatization;
2006-09-18 obua 2006-09-18 replaced implodeable_Ext by set_like
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-03-07 obua 2006-03-07 Added HOL-ZF to Isabelle.