src/HOL/ZF/HOLZF.thy
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.