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