src/HOL/RelPow.ML
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-03-30 oheimb 1998-03-30 added Univalent_rel_pow
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-05-30 paulson 1997-05-30 Overloading of "^" requires a type constraint
1997-04-23 paulson 1997-04-23 Ran expandshort
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-03-06 pusch 1997-03-06 Minor changes due to primrec definition for ^
1996-10-07 paulson 1996-10-07 Removed commands made redundant by new one-point rules
1996-09-26 paulson 1996-09-26 Ran expandshort
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-04-27 nipkow 1996-04-27 Added R^1 = R
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-02-19 nipkow 1996-02-19 Introduced normalize_thm into HOL.ML Corrected some dependencies among Sum, Prod and mono. Extended RelPow
1996-02-15 nipkow 1996-02-15 Added a few thms and the new theory RelPow.