src/HOL/Set.thy
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2004-04-13 ballarin 2004-04-13 Various changes to HOL-Algebra; Locale instantiation.
2004-03-24 paulson 2004-03-24 streamlined treatment of quotients for the integers
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-02-11 nipkow 2004-02-11 Modified UN and INT xsymbol syntax: made index subscript
2004-01-01 paulson 2004-01-01 conversion of Real/PReal to Isar script; type "complex" is now in class "field"
2003-12-19 nipkow 2003-12-19 *** empty log message ***
2003-09-26 paulson 2003-09-26 misc tidying
2003-07-11 oheimb 2003-07-11 added rev_ballE
2003-03-17 paulson 2003-03-17 moved one proof, added another
2003-03-14 paulson 2003-03-14 new UN/INT simprules
2003-03-11 nipkow 2003-03-11 *** empty log message ***
2003-02-26 paulson 2003-02-26 new lemma
2003-02-25 nipkow 2003-02-25 Undid eta change for UN/INT.
2003-02-16 paulson 2003-02-16 new theorem Compl_partition2
2002-12-22 nipkow 2002-12-22 removed some problems with print translations
2002-12-22 nipkow 2002-12-22 added print translations tha avoid eta contraction for important binders.
2002-10-18 nipkow 2002-10-18 Added a few thms about UN/INT/{}/UNIV
2002-10-03 paulson 2002-10-03 added the new elim rule psubsetE
2002-08-30 paulson 2002-08-30 removal of blast.overloaded
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-07-24 wenzelm 2002-07-24 simplified locale predicates;
2002-05-07 wenzelm 2002-05-07 rev_bexI [intro?];
2002-05-06 nipkow 2002-05-06 Added insert_disjoint and disjoint_insert [simp], and simplified proofs
2002-02-25 wenzelm 2002-02-25 clarified syntax of ``long'' statements: fixes/assumes/shows;
2002-02-16 wenzelm 2002-02-16 converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
2002-01-04 wenzelm 2002-01-04 tuned ``syntax (output)'';
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-21 wenzelm 2001-11-21 theory Inverse_Image converted and moved to Set;
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2001-11-03 wenzelm 2001-11-03 tuned;
2001-11-02 wenzelm 2001-11-02 theory Calculation move to Set;
2001-10-30 wenzelm 2001-10-30 lemma Least_mono moved from Typedef.thy to Set.thy;
2001-10-28 wenzelm 2001-10-28 converted theory "Set";
2001-10-14 wenzelm 2001-10-14 removed Ord;
2001-01-28 nipkow 2001-01-28 fixed set comprehension print translation
2001-01-09 nipkow 2001-01-09 `` -> and ``` -> ``
2000-10-03 wenzelm 2000-10-03 range declared as syntax;
2000-09-28 wenzelm 2000-09-28 fixed \<Union>, \<Inter> syntax;
2000-01-28 oheimb 2000-01-28 beautified spacing for binders with symbols syntax, analogous to HOL.thy
1999-11-11 paulson 1999-11-11 new-style infix declaration for "image"
1999-08-26 paulson 1999-08-26 a little tidying; also FIXED BAD TYPE in INTER1, UNION1
1999-08-17 wenzelm 1999-08-17 replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal);
1998-11-18 paulson 1998-11-18 Finally removing "Compl" from HOL
1998-10-30 paulson 1998-10-30 Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
1998-08-05 paulson 1998-08-05 Removal of "disjoint" translation
1998-08-04 wenzelm 1998-08-04 fixed disjount translation;
1998-07-15 nipkow 1998-07-15 Minor tidying up.
1998-03-30 oheimb 1998-03-30 added caveat
1997-11-05 paulson 1997-11-05 UNIV now a constant; UNION1, INTER1 now translations and no longer have separate rules for themselves
1997-11-05 wenzelm 1997-11-05 adapted typed_print_translation;
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-10-09 wenzelm 1997-10-09 fixed infix syntax;
1997-05-30 paulson 1997-05-30 Overloading of "^" requires new type class "power", with types "nat" and "set" in that class. The operator itself is declared in Nat.thy
1997-05-16 nipkow 1997-05-16 Distributed Psubset stuff to basic set theory files, incl Finite. Added stuff by bu.
1997-04-16 wenzelm 1997-04-16 improved translations for subset symbols syntax: constraints;
1997-04-04 nipkow 1997-04-04 moved inj and surj from Set to Fun and Inv -> inv.
1997-02-25 wenzelm 1997-02-25 added proper subset symbols syntax;