src/HOL/Set.ML
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
1997-10-17 nipkow 1997-10-17 Added image_eqI to simpset.
1997-10-16 nipkow 1997-10-16 Modified comment.
1997-10-16 nipkow 1997-10-16 Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-26 paulson 1997-09-26 Minor tidying to use Clarify_tac, etc.
1997-08-01 nipkow 1997-08-01 Added {x.x=a} = a to !simpset.
1997-07-01 paulson 1997-07-01 Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
1997-06-06 paulson 1997-06-06 New miniscoping rules ball_triv and bex_triv
1997-05-16 nipkow 1997-05-16 Distributed Psubset stuff to basic set theory files, incl Finite. Added stuff by bu.
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-04-04 nipkow 1997-04-04 moved inj and surj from Set to Fun and Inv -> inv.
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1997-04-03 paulson 1997-04-03 Declares overloading for set-theoretic constants
1997-04-02 paulson 1997-04-02 Re-ordering of rules to assist blast_tac Powerset rules must not be the most recent
1997-03-05 paulson 1997-03-05 New version of InterE, like its ZF counterpart
1997-02-12 nipkow 1997-02-12 New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
1997-01-09 paulson 1997-01-09 Tidying of proofs. New theorems are enterred immediately into the relevant clasets or simpsets.
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-25 paulson 1996-09-25 Rationalized the rewriting of membership for {} and insert by deleting the redundant theorems in_empty and in_insert
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
1996-08-22 paulson 1996-08-22 Proved mem_if