src/HOL/ex/set.thy
2011-01-07 bulwahn 2011-01-07 removing obselete Id comments from HOL/ex theories
2010-12-03 wenzelm 2010-12-03 recoded latin1 as utf8; use textcomp for some text symbols where it appears appropriate;
2010-12-03 krauss 2010-12-03 eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended
2010-04-23 wenzelm 2010-04-23 mark schematic statements explicitly;
2009-12-10 paulson 2009-12-10 streamlined proofs
2009-10-22 nipkow 2009-10-22 inv_onto -> inv_into
2009-10-18 nipkow 2009-10-18 Inv -> inv_onto, inv abbr. inv_onto UNIV.
2007-10-05 nipkow 2007-10-05 added lemmas
2007-09-14 paulson 2007-09-14 tidied
2006-07-04 ballarin 2006-07-04 Typo.
2005-12-13 paulson 2005-12-13 meson no longer does these examples
2005-07-20 paulson 2005-07-20 revised examples
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-02-02 paulson 2005-02-02 tidying of some subst/simplesubst proofs
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-11-22 nipkow 2004-11-22 fixed proof
2004-01-12 paulson 2004-01-12 Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers
2002-05-07 wenzelm 2002-05-07 tuned presentation;
2002-03-14 paulson 2002-03-14 converted theory "set" to Isar and added some SET-VAR examples
2000-06-21 wenzelm 2000-06-21 fixed deps;