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