src/HOL/Induct/LList.ML
Mon, 30 Nov 1998 10:44:05 +0100 paulson Renamed subset_Sigma_llist to subset_Times_llist
Thu, 26 Nov 1998 17:40:10 +0100 paulson tidied up list definitions, using type 'a option instead of
Mon, 02 Nov 1998 15:31:29 +0100 paulson Domain r, Range r replace fst``r, snd``r
Thu, 06 Aug 1998 15:48:13 +0200 paulson even more tidying of Goal commands
Fri, 24 Jul 1998 13:19:38 +0200 berghofe Adapted to new datatype package.
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
Tue, 30 Jun 1998 20:51:15 +0200 berghofe Adapted to new inductive definition package.
Fri, 26 Jun 1998 15:16:14 +0200 paulson New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
Thu, 25 Jun 1998 16:13:20 +0200 wenzelm delsimprocs [unit_eq_proc];
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Mon, 27 Apr 1998 16:45:27 +0200 nipkow Renamed expand_const -> split_const.
Tue, 21 Apr 1998 17:23:24 +0200 oheimb split_all_tac is now added to claset() _before_ other safe tactics
Thu, 08 Jan 1998 11:21:45 +0100 paulson Tidied by adding more default simprules
Wed, 24 Dec 1997 10:02:30 +0100 paulson New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
Wed, 05 Nov 1997 13:45:01 +0100 paulson Adapted to removal of UN1_I, etc
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp;
Fri, 17 Oct 1997 15:25:12 +0200 nipkow setloop split_tac -> addsplits
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Fri, 06 Jun 1997 13:28:40 +0200 paulson Removed a few redundant additions of simprules or classical rules
Wed, 07 May 1997 12:50:26 +0200 paulson New directory to contain examples of (co)inductive definitions
less more (0) tip