| Fri, 01 Dec 2000 11:02:55 +0100 | paulson | renamed less_eq_Suc_add to less_imp_Suc_add | file | diff | annotate |
| Wed, 30 Aug 2000 16:29:21 +0200 | nipkow | introduced induct_thm_tac | file | diff | annotate |
| Tue, 16 May 2000 14:07:49 +0200 | paulson | changed to cope with the rewriting of #2+n to Suc(Suc n) | file | diff | annotate |
| Thu, 04 May 2000 15:17:41 +0200 | paulson | from Suc...Suc to #m | file | diff | annotate |
| Tue, 02 May 2000 18:55:11 +0200 | paulson | modified for new simprocs | file | diff | annotate |
| Thu, 30 Mar 2000 19:45:51 +0200 | nipkow | recdef.rules -> recdef.simps | file | diff | annotate |
| Mon, 13 Mar 2000 16:23:34 +0100 | wenzelm | case_tac now subsumes both boolean and datatype cases; | file | diff | annotate |
| Mon, 13 Mar 2000 12:51:10 +0100 | nipkow | exhaust_tac -> cases_tac | file | diff | annotate |
| Fri, 27 Nov 1998 17:00:30 +0100 | nipkow | At last: linear arithmetic for nat! | file | diff | annotate |
| Thu, 01 Oct 1998 18:29:38 +0200 | paulson | tidied | file | diff | annotate |
| Thu, 10 Sep 1998 17:32:07 +0200 | paulson | a step to help a proof | file | diff | annotate |
| Wed, 15 Jul 1998 14:19:02 +0200 | paulson | More tidying and removal of "\!\!... from Goal commands | file | diff | annotate |
| Wed, 15 Jul 1998 10:15:13 +0200 | paulson | Removal of leading "\!\!..." from most Goal commands | file | diff | annotate |
| Thu, 25 Jun 1998 13:57:34 +0200 | paulson | Installation of target HOL-Real | file | diff | annotate |
| Mon, 22 Jun 1998 17:26:46 +0200 | wenzelm | isatool fixgoal; | file | diff | annotate |
| Wed, 05 Nov 1997 13:23:46 +0100 | paulson | Ran expandshort, especially to introduce Safe_tac | file | diff | annotate |
| Mon, 03 Nov 1997 12:13:18 +0100 | wenzelm | isatool fixclasimp; | file | diff | annotate |
| Mon, 23 Jun 1997 10:42:03 +0200 | paulson | Ran expandshort | file | diff | annotate |
| Mon, 26 May 1997 12:33:03 +0200 | paulson | New example ported from ZF | file | diff | annotate |