src/HOL/Lambda/Commutation.ML
1997-04-04 paulson 1997-04-04 Now calls blast_tac
1996-10-07 paulson 1996-10-07 Ran expandshort
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-11 nipkow 1996-09-11 Removed refs to clasets like rel_cs etc. Used implicit claset.
1996-04-04 paulson 1996-04-04 For renaming to rtrancl_Un_rtrancl
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-02 nipkow 1996-01-02 Polished proofs.
1995-10-25 nipkow 1995-10-25 Moved some thms to Arith and to Trancl.
1995-10-11 nipkow 1995-10-11 Commutation replaces Confluence