src/HOL/Lambda/Commutation.ML
Wed, 23 Apr 1997 11:20:18 +0200 paulson Necessary inclusion of depth bound into blast_tac call
Wed, 09 Apr 1997 12:32:04 +0200 paulson Using Blast_tac
Fri, 04 Apr 1997 12:21:28 +0200 paulson Now calls blast_tac
Mon, 07 Oct 1996 10:31:50 +0200 paulson Ran expandshort
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Wed, 11 Sep 1996 15:17:07 +0200 nipkow Removed refs to clasets like rel_cs etc. Used implicit claset.
Thu, 04 Apr 1996 11:43:25 +0200 paulson For renaming to rtrancl_Un_rtrancl
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Tue, 02 Jan 1996 14:08:04 +0100 nipkow Polished proofs.
Wed, 25 Oct 1995 09:49:35 +0100 nipkow Moved some thms to Arith and to Trancl.
Wed, 11 Oct 1995 10:09:56 +0100 nipkow Commutation replaces Confluence
less more (0) tip