src/HOL/mono.ML
1999-07-27 wenzelm 1999-07-27 fixed comments;
1999-07-23 nipkow 1999-07-23 New lemmas by Stefan Merz.
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-06-30 berghofe 1998-06-30 Removed obsolete comments.
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-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-04-09 paulson 1997-04-09 Using Blast_tac
1996-07-11 paulson 1996-07-11 Added insert_mono
1996-05-23 berghofe 1996-05-23 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-02-19 nipkow 1996-02-19 Introduced normalize_thm into HOL.ML Corrected some dependencies among Sum, Prod and mono. Extended RelPow
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-03-03 clasohm 1995-03-03 new version of HOL with curried function application