1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-04-07 oheimb 1998-04-07 made split_all_tac as safe wrapper more defensive: if it is added as unsafe wrapper again (as its was before), this does not break the current proofs.
1998-04-02 oheimb 1998-04-02 split_all_tac now fails if there is nothing to split split_all_tac has moved within claset() from usafe wrappers to safe wrappers
1998-03-30 oheimb 1998-03-30 generalized appearance of trancl_into_rtrancl and r_into_trancl added irrefl_tranclI, reflcl_trancl, trancl_reflcl, trancl_empty, rtrancl_empty
1998-03-16 paulson 1998-03-16 inverse -> converse [It is standard terminology and also used in ZF]
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-09-29 paulson 1997-09-29 Tidied proof of r_comp_rtrancl_eq
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-06-17 nipkow 1997-06-17 converse -> ^-1
1997-06-05 nipkow 1997-06-05 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. Relation.ML Trancl.ML: more thms WF.ML WF.thy: added `acyclic' WF_Rel.ML: moved some thms back into WF and added some new ones.
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-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