src/HOL/Set.ML
1997-12-24 ago New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-23 ago Overloading info for image
1997-12-18 ago UNIV_I no longer counts as safe
1997-12-16 ago expandshort;
1997-11-20 ago Renamed "overload" to "overloaded" for sml/nj compatibility
1997-11-16 ago Removed
1997-11-15 ago Added
1997-11-05 ago UNIV now a constant; UNION1, INTER1 now translations and no longer have
1997-11-04 ago removed redundant ball_empty and bex_empty (see equalities.ML)
1997-11-03 ago isatool fixclasimp;
1997-11-01 ago New Blast_tac (and minor tidying...)
1997-10-21 ago New rewrite rules image_iff
1997-10-17 ago setloop split_tac -> addsplits
1997-10-17 ago New rewrite rules for simplifying conditionals
1997-10-17 ago Added image_eqI to simpset.
1997-10-16 ago Modified comment.
1997-10-16 ago Various new lemmas. Improved conversion of equations to rewrite rules:
1997-10-10 ago fixed dots;
1997-09-26 ago Minor tidying to use Clarify_tac, etc.
1997-08-01 ago Added {x.x=a} = a to !simpset.
1997-07-01 ago Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
1997-06-06 ago New miniscoping rules ball_triv and bex_triv
1997-05-16 ago Distributed Psubset stuff to basic set theory files, incl Finite.
1997-04-11 ago Yet more fast_tac->blast_tac, and other tidying
1997-04-04 ago moved inj and surj from Set to Fun and Inv -> inv.
1997-04-04 ago Calls Blast_tac
1997-04-03 ago Declares overloading for set-theoretic constants
1997-04-02 ago Re-ordering of rules to assist blast_tac
1997-03-05 ago New version of InterE, like its ZF counterpart
1997-02-12 ago New class "order" and accompanying changes.
1997-01-09 ago Tidying of proofs. New theorems are enterred immediately into the
1996-09-26 ago Ran expandshort
1996-09-25 ago Rationalized the rewriting of membership for {} and insert
1996-09-12 ago Tidied many proofs, using AddIffs to let equivalences take
1996-08-22 ago Proved mem_if
1996-08-19 ago Added impOfSubs
1996-07-26 ago Proved bex_False
1996-06-28 ago Added contra_subsetD and rev_contra_subsetD
1996-06-18 ago New rewrites for vacuous quantification
1996-05-31 ago moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
1996-05-23 ago equalityI is now added to default claset
1996-05-23 ago Replaced fast_tac by Fast_tac (which uses default claset)
1996-04-04 ago Added more _iff rewrites for Compl, Un, Int
1996-03-27 ago Library changes for mutilated checkerboard
1996-03-06 ago Ran expandshort
1996-03-06 ago Added 'section' commands
1996-03-04 ago Added a constant UNIV == {x.True}
1996-01-30 ago expanded tabs
1995-03-03 ago new version of HOL with curried function application