src/HOL/ZF/Games.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)
2012-02-21 haftmann 2012-02-21 reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
2012-02-20 haftmann 2012-02-20 tuned proof
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-08-02 krauss 2011-08-02 eliminated obsolete recdef/wfrec related declarations
2011-02-18 wenzelm 2011-02-18 more precise headers;
2011-01-12 wenzelm 2011-01-12 eliminated global prems; tuned proofs;
2010-11-30 haftmann 2010-11-30 adapted fragile proof
2010-10-01 haftmann 2010-10-01 constant `contents` renamed to `the_elem`
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-03-02 krauss 2010-03-02 killed more recdefs
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-03-02 nipkow 2009-03-02 name changes
2008-07-25 haftmann 2008-07-25 tuned
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts;
2008-01-02 haftmann 2008-01-02 removed some legacy instantiations
2007-07-11 berghofe 2007-07-11 Restored set notation in Multiset theory.
2007-02-07 berghofe 2007-02-07 - Adapted to new inductive definition package - Adapted to changes in Multiset theory
2006-06-05 krauss 2006-06-05 Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.
2006-03-07 obua 2006-03-07 Added HOL-ZF to Isabelle.