src/HOL/Set.thy
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-06 nipkow 2004-08-06 undid UN/INT syntax
2004-08-03 paulson 2004-08-03 new simprules Int_subset_iff and Un_subset_iff
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-29 wenzelm 2004-05-29 \<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-28 paulson 2004-05-28 new theorem Collect_imp_eq
2004-05-26 nipkow 2004-05-26 Corrected printer bug for bounded quantifiers Q x<=y. P
2004-05-17 mehta 2004-05-17 lemma disjoint_int_union removed - too special
2004-05-13 mehta 2004-05-13 New simp rules added: insert_disjoint disjoint_insert disjoint_int_union
2004-05-01 wenzelm 2004-05-01 improved subscript syntax;
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.