| Fri, 26 May 2000 18:05:34 +0200 | paulson | addss -> force_tac | file | diff | annotate |
| Fri, 03 Jul 1998 10:36:47 +0200 | nipkow | Removed leading !! in goals. | file | diff | annotate |
| Mon, 22 Jun 1998 17:26:46 +0200 | wenzelm | isatool fixgoal; | file | diff | annotate |
| Mon, 16 Mar 1998 16:50:50 +0100 | paulson | inverse -> converse | file | diff | annotate |
| Tue, 23 Dec 1997 11:50:36 +0100 | paulson | Tidied. Also better proof using new blast_tac | file | diff | annotate |
| Mon, 03 Nov 1997 12:13:18 +0100 | wenzelm | isatool fixclasimp; | file | diff | annotate |
| Tue, 17 Jun 1997 09:01:56 +0200 | nipkow | converse -> ^-1 | file | diff | annotate |
| Wed, 23 Apr 1997 11:20:18 +0200 | paulson | Necessary inclusion of depth bound into blast_tac call | file | diff | annotate |
| Wed, 09 Apr 1997 12:32:04 +0200 | paulson | Using Blast_tac | file | diff | annotate |
| Fri, 04 Apr 1997 12:21:28 +0200 | paulson | Now calls blast_tac | file | diff | annotate |
| Mon, 07 Oct 1996 10:31:50 +0200 | paulson | Ran expandshort | file | diff | annotate |
| Thu, 26 Sep 1996 12:47:47 +0200 | paulson | Ran expandshort | file | diff | annotate |
| Wed, 11 Sep 1996 15:17:07 +0200 | nipkow | Removed refs to clasets like rel_cs etc. Used implicit claset. | file | diff | annotate |
| Thu, 04 Apr 1996 11:43:25 +0200 | paulson | For renaming to rtrancl_Un_rtrancl | file | diff | annotate |
| Tue, 30 Jan 1996 15:24:36 +0100 | clasohm | expanded tabs | file | diff | annotate |
| Tue, 02 Jan 1996 14:08:04 +0100 | nipkow | Polished proofs. | file | diff | annotate |
| Wed, 25 Oct 1995 09:49:35 +0100 | nipkow | Moved some thms to Arith and to Trancl. | file | diff | annotate |
| Wed, 11 Oct 1995 10:09:56 +0100 | nipkow | Commutation replaces Confluence | file | diff | annotate |