src/HOL/Relation.ML
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
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-06-28 paulson 1996-06-28 Removed the unused rel_eq_cs
1996-06-03 berghofe 1996-06-03 best_tac, deepen_tac and safe_tac now also use default claset.
1996-05-23 berghofe 1996-05-23 Removed equalityI from some proofs (because it is now included in the default claset)
1996-05-21 berghofe 1996-05-21 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_O_id and id_O_R
1996-04-04 paulson 1996-04-04 Using new "Times" infix
1996-03-25 nipkow 1996-03-25 added converse_converse
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-26 nipkow 1996-01-26 Streamlined defs in Relation and added new intro/elim rules to do with pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-05-26 nipkow 1995-05-26 Trancl is now based on Relation which used to be in Integ.