src/HOL/Set.ML
2002-10-18 nipkow 2002-10-18 Added a few thms about UN/INT/{}/UNIV
2002-02-16 wenzelm 2002-02-16 converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
2001-11-21 wenzelm 2001-11-21 theory Inverse_Image converted and moved to Set;
2001-10-28 wenzelm 2001-10-28 converted theory "Set";
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-14 wenzelm 2001-10-14 improved atomize setup;
2001-10-03 wenzelm 2001-10-03 tuned parentheses in relational expressions;
2001-09-27 wenzelm 2001-09-27 AddXEs [UnI1, UnI2];
2001-05-08 paulson 2001-05-08 fixed comment
2001-03-29 nipkow 2001-03-29 generalization of 1 point rules for ALL
2001-03-27 nipkow 2001-03-27 fixed bug in tactic for ball 1 point simproc
2001-03-26 nipkow 2001-03-26 I forgot a few bases cases for the 1-point rules...
2001-03-23 nipkow 2001-03-23 added one point simprocs for bounded quantifiers
2001-02-20 oheimb 2001-02-20 simplified definition of wrapper bspec
2001-01-31 oheimb 2001-01-31 added diff_single_insert and subset_image_iff
2001-01-09 nipkow 2001-01-09 `` -> and ``` -> ``
2000-11-17 wenzelm 2000-11-17 UNIV_witness;
2000-10-17 paulson 2000-10-17 tidying; removed unused rev_contra_subsetD
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-09-07 wenzelm 2000-09-07 updated rulify setup;
2000-09-01 wenzelm 2000-09-01 fixed rulify_prems;
2000-08-25 paulson 2000-08-25 moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
2000-07-24 wenzelm 2000-07-24 avoid referencing thy value;
2000-07-17 wenzelm 2000-07-17 AddXIs [UnI1, UnI2];
2000-07-14 oheimb 2000-07-14 re-added subset_empty to simpset
2000-06-29 paulson 2000-06-29 now uses equalityCE, which usually is more efficent than equalityE
2000-06-28 paulson 2000-06-28 deleted a redundant bind_thm
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-06-20 paulson 2000-06-20 replaced the useless [p]subset_insertD by [p]subset_insert_iff
2000-06-16 paulson 2000-06-16 Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT
2000-06-07 paulson 2000-06-07 tidied
2000-05-22 paulson 2000-05-22 psubsetI is a safe rule
2000-05-08 wenzelm 2000-05-08 strip = impI allI allI;
2000-03-02 paulson 2000-03-02 tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and installed them by AddIffs, since they are an important special case of equalityE.
1999-12-08 paulson 1999-12-08 useful lemma eqset_imp_iff
1999-11-23 paulson 1999-11-23 new theorem rev_image_eqI
1999-11-11 paulson 1999-11-11 new-style infix declaration for "image"
1999-11-05 paulson 1999-11-05 new psubset lemma
1999-10-29 oheimb 1999-10-29 improved singleton_insert_inj_eq
1999-10-05 berghofe 1999-10-05 Added attribute rulify_prems (useful for modifying premises of introduction rules of inductive sets).
1999-09-29 wenzelm 1999-09-29 CollectE; AddXIs [subsetD, rev_subsetD, psubsetI];
1999-09-07 wenzelm 1999-09-07 isatool expandshort;
1999-09-06 oheimb 1999-09-06 added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
1999-09-02 wenzelm 1999-09-02 AddXDs [bspec];
1999-07-19 paulson 1999-07-19 getting rid of qed_goal
1999-07-15 paulson 1999-07-15 qed_goal -> Goal
1999-04-16 wenzelm 1999-04-16 lemmas about proper subset relation;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-03 paulson 1999-03-03 expandshort
1999-03-01 paulson 1999-03-01 simpler proofs of congruence rules
1999-02-03 paulson 1999-02-03 inj is now a translation of inj_on
1998-12-02 paulson 1998-12-02 new rule rev_bexI
1998-11-18 paulson 1998-11-18 Finally removing "Compl" from HOL
1998-10-15 paulson 1998-10-15 Uses overload_1st_set to specify overloading
1998-10-01 nipkow 1998-10-01 new singleton_conv2
1998-09-21 oheimb 1998-09-21 added wrapper for bspec
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
1998-09-10 paulson 1998-09-10 Changed equals0E back to equals0D and gave it the correct destruct form
1998-08-19 paulson 1998-08-19 fixed overloading of "image"
1998-08-14 paulson 1998-08-14 expandshort