src/HOL/List.thy
Wed, 24 Jun 1998 13:59:45 +0200 nipkow * HOL/List: new function list_update written xs[i:=v] that updates the i-th
Sun, 22 Feb 1998 14:12:23 +0100 nipkow New induction schemas for lists (length and snoc).
Fri, 06 Feb 1998 18:55:18 +0100 nipkow Added `remdups'
Tue, 30 Dec 1997 11:14:09 +0100 nipkow nth -> !
Wed, 05 Nov 1997 11:49:34 +0100 wenzelm adapted typed_print_translation;
Tue, 04 Nov 1997 20:47:38 +0100 oheimb added zip and nodup
Thu, 16 Oct 1997 14:12:15 +0200 nipkow Various new lemmas. Improved conversion of equations to rewrite rules:
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Tue, 05 Aug 1997 16:21:45 +0200 nipkow Added function `replicate' and lemmas map_cong and set_replicate.
Fri, 01 Aug 1997 09:42:19 +0200 nipkow Corected bug in def of dropWhile (also present in Haskell lib!)
Wed, 09 Jul 1997 12:57:04 +0200 nipkow Improved length = size translation.
Thu, 26 Jun 1997 13:20:50 +0200 nipkow set_of_list -> set
Mon, 16 Jun 1997 14:24:11 +0200 paulson Replacing the primrec definition of "length" by a translation to the built-in
Thu, 05 Jun 1997 13:20:18 +0200 paulson Deleted the obsolete "pred_list" relation
Fri, 30 May 1997 15:16:44 +0200 paulson Now Divides must be the parent
Mon, 26 May 1997 12:38:29 +0200 paulson New operator "lists" for formalizing sets of lists
Fri, 23 May 1997 18:17:53 +0200 nipkow Added `arbitrary'
Thu, 15 May 1997 12:54:02 +0200 paulson Added pred_list for TFL
Thu, 06 Mar 1997 16:04:23 +0100 pusch primrec definition for nth
Wed, 12 Feb 1997 18:53:59 +0100 nipkow New class "order" and accompanying changes.
Fri, 17 Jan 1997 10:09:46 +0100 nipkow Got rid of Alls in List.
Tue, 10 Dec 1996 14:16:11 +0100 wenzelm removed ambiguous symbols syntax;
Wed, 27 Nov 1996 17:00:25 +0100 wenzelm added symbols syntax;
Mon, 19 Aug 1996 11:12:38 +0200 paulson Renamed setOfList to set_of_list
Fri, 02 Aug 1996 12:16:11 +0200 berghofe Simplified primrec definitions.
Tue, 25 Jun 1996 13:11:29 +0200 berghofe Changed argument order of nat_rec.
Tue, 18 Jun 1996 16:20:30 +0200 paulson Addition of setOfList
Mon, 05 Feb 1996 21:27:16 +0100 clasohm expanded tabs; renamed subtype to typedef;
Fri, 22 Dec 1995 12:25:20 +0100 nipkow defined take/drop by induction over list rather than nat.
Wed, 29 Nov 1995 16:44:59 +0100 clasohm removed quotes from types in consts and syntax sections
Sun, 12 Nov 1995 16:29:12 +0100 nipkow added new arithmetic lemmas and the functions take and drop.
Thu, 29 Jun 1995 16:33:17 +0200 lcp Added function rev and its properties length_rev, etc.
Tue, 28 Mar 1995 12:25:20 +0200 clasohm changed syntax of datatype declarations (curried types for constructor
Mon, 20 Mar 1995 15:35:28 +0100 clasohm changed syntax of "if"
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application
less more (0) tip