src/HOL/ex/set.ML
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2000-10-12 paulson 2000-10-12 tidied
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-07-13 wenzelm 2000-07-13 fixed comment;
2000-06-29 paulson 2000-06-29 tidied proofs using default rule equalityCE
2000-06-28 paulson 2000-06-28 tidied
2000-06-21 wenzelm 2000-06-21 fixed deps;
2000-02-21 paulson 2000-02-21 new examples that cannot be done in LEO
1999-08-27 paulson 1999-08-27 the bij predicate forced renaming of a variable bij
1999-02-05 paulson 1999-02-05 tidied Schroeder-Bernstein proof
1999-02-03 paulson 1999-02-03 inj is now a translation of inj_on
1999-01-20 paulson 1999-01-20 renamed variables for clarity
1998-11-02 paulson 1998-11-02 increased precedence of unary minus from 80 to 100
1998-10-22 paulson 1998-10-22 standard Blast_tac demos
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
1998-09-07 paulson 1998-09-07 new example; tidying
1998-04-27 nipkow 1998-04-27 Renamed expand_const -> split_const.
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1997-11-28 paulson 1997-11-28 New example
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-04 wenzelm 1997-11-04 isatool fixclasimp;
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-04-21 paulson 1997-04-21 New blast_tac demo
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-04-04 nipkow 1997-04-04 Inv -> inv
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-07-26 paulson 1996-07-26 Removal of cfast_tac
1996-06-21 berghofe 1996-06-21 Classical tactics now use default claset.
1996-02-09 nipkow 1996-02-09 replace sstac
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-03-22 clasohm 1995-03-22 converted ex with curried function application