| Mon, 26 May 1997 12:39:57 +0200 | paulson | Renamed lessD to Suc_leI | file | diff | annotate |
| Tue, 20 May 1997 11:41:01 +0200 | paulson | Some theorems moved to HOL/Arith.ML | file | diff | annotate |
| Thu, 24 Apr 1997 18:06:46 +0200 | nipkow | Introduced a generic "induct_tac" which picks up the right induction scheme | file | diff | annotate |
| Thu, 26 Sep 1996 12:47:47 +0200 | paulson | Ran expandshort | file | diff | annotate |
| Fri, 19 Jul 1996 15:56:01 +0200 | berghofe | Classical tactics now use default claset. | file | diff | annotate |
| Wed, 01 May 1996 13:55:20 +0200 | paulson | Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith. | file | diff | annotate |
| Mon, 05 Feb 1996 21:29:06 +0100 | clasohm | expanded tabs; incorporated Konrad's changes | file | diff | annotate |
| Tue, 30 Jan 1996 15:24:36 +0100 | clasohm | expanded tabs | file | diff | annotate |
| Fri, 17 Nov 1995 09:04:10 +0100 | nipkow | New directory. | file | diff | annotate |