src/HOL/RelPow.ML
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.