src/HOL/equalities.ML
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-01-17 paulson 1997-01-17 New rewrites for bounded quantifiers
1997-01-17 paulson 1997-01-17 New miniscoping rules for the bounded quantifiers and UN/INT operators
1997-01-17 nipkow 1997-01-17 Got rid of Alls in List. Added Ball_insert and Ball_Un in equalities.ML.
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-24 paulson 1996-09-24 Added miniscoping for UN and INT
1996-08-19 paulson 1996-08-19 Added proof of Un_insert_right
1996-07-26 paulson 1996-07-26 Proved insert_image
1996-07-22 paulson 1996-07-22 Added insert_commute
1996-06-28 paulson 1996-06-28 Removed the unused eq_cs, and added some distributive laws
1996-06-03 berghofe 1996-06-03 best_tac, deepen_tac and safe_tac now also use default claset.
1996-05-23 berghofe 1996-05-23 expanded TABs
1996-05-21 berghofe 1996-05-21 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-05-17 nipkow 1996-05-17 Added if_image_distrib.
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-03-27 paulson 1996-03-27 Library changes for mutilated checkerboard
1996-03-11 paulson 1996-03-11 Deleted faulty comment; proved new rule Inter_Un_subset
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-03-06 nipkow 1996-03-06 Added 'section' commands
1996-03-04 nipkow 1996-03-04 Added a constant UNIV == {x.True} Added many new rewrite rules for sets. Moved LEAST into Nat. Added cardinality to Finite.
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-07-05 nipkow 1995-07-05 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application