src/HOL/Set.ML
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
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-12 oheimb 1998-08-12 cleanup for Fun.thy: merged Update.{thy|ML} into Fun.{thy|ML} moved o_def from HOL.thy to Fun.thy added Id_def to Fun.thy moved image_compose from Set.ML to Fun.ML moved o_apply and o_assoc from simpdata.ML to Fun.ML moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML added fun_upd_twist to Fun.ML
1998-08-06 paulson 1998-08-06 Now recognizes both {}= and ={}
1998-08-05 paulson 1998-08-05 Renamed equals0D to equals0E
1998-08-04 paulson 1998-08-04 Deleted the redundant rule mem_if
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-04-02 paulson 1998-04-02 changed if_bool_eq to if_bool_eq_conj
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1998-01-08 paulson 1998-01-08 New rule: image_subset
1998-01-02 paulson 1998-01-02 New theorem image_subsetI
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort