src/HOL/Set.ML
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
1997-12-23 paulson 1997-12-23 Overloading info for image
1997-12-18 paulson 1997-12-18 UNIV_I no longer counts as safe
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-11-20 paulson 1997-11-20 Renamed "overload" to "overloaded" for sml/nj compatibility
1997-11-16 nipkow 1997-11-16 Removed "(ALL x:f``A. P x) = (ALL x:A. P(f x))", "(EX x:f``A. P x) = (EX x:A. P(f x))", again, because they were already there and added "(UN x:f``A. B x) = (UN a:A. B(f a))" "(INT x:f``A. B x) = (INT a:A. B(f a))" instead.
1997-11-15 nipkow 1997-11-15 Added > "(? x : f `` A. P x) = (? a:A. P(f a))" > "(! x : f `` A. P x) = (! a:A. P(f a))"
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-04 oheimb 1997-11-04 removed redundant ball_empty and bex_empty (see equalities.ML)
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-10-21 paulson 1997-10-21 New rewrite rules image_iff
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-17 paulson 1997-10-17 New rewrite rules for simplifying conditionals