src/HOL/Trancl.ML
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
1996-08-19 paulson 1996-08-19 Tidied up the proofs
1996-06-03 berghofe 1996-06-03 best_tac, deepen_tac and safe_tac now also use default claset.
1996-05-24 nipkow 1996-05-24 Modified proof of "(R^=)^* = R^*" to accommodate equalityI.
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-05-17 nipkow 1996-05-17 Moved split_rule et al from ind_syntax.ML to Prod.ML. Used split_rule in Lfp.ML and Trancl.ML.
1996-04-30 nipkow 1996-04-30 Added backwards rtrancl_induct and special versions for pairs.
1996-04-04 paulson 1996-04-04 Using new "Times" infix
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-02-15 nipkow 1996-02-15 Added a few thms and the new theory RelPow.
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-25 nipkow 1995-10-25 Added various thms and tactics.
1995-05-28 nipkow 1995-05-28 Added trancl_cs
1995-05-26 nipkow 1995-05-26 Trancl is now based on Relation which used to be in Integ.
1995-05-15 nipkow 1995-05-15 renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans.
1995-05-13 nipkow 1995-05-13 Added some lemmas about r^*.
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application