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