Thu, 26 Jan 1995 10:41:21 +0100 |
nipkow |
Added "nth" and some lemmas.
|
file |
diff |
annotate
|
Fri, 02 Dec 1994 16:13:34 +0100 |
nipkow |
Moved the old List to ex and replaced it by one defined via
|
file |
diff |
annotate
|
Thu, 25 Aug 1994 11:01:45 +0200 |
lcp |
INSTALLATION OF INDUCTIVE DEFINITIONS
|
file |
diff |
annotate
|
Thu, 18 Aug 1994 12:42:19 +0200 |
lcp |
HOL/List: rotated arguments of List_case, list_case
|
file |
diff |
annotate
|
Wed, 30 Mar 1994 10:00:23 +0200 |
nipkow |
@ now associates to the right, just like #, in order to avoid loss of
|
file |
diff |
annotate
|
Thu, 17 Mar 1994 11:27:29 +0100 |
clasohm |
adapted type definition to new syntax
|
file |
diff |
annotate
|
Wed, 02 Mar 1994 12:26:55 +0100 |
clasohm |
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
|
file |
diff |
annotate
|
Sat, 12 Feb 1994 14:46:21 +0100 |
nipkow |
added translations for "case xs of"
|
file |
diff |
annotate
|
Thu, 03 Feb 1994 09:55:47 +0100 |
nipkow |
Introduction of various new lemmas and of case_tac.
|
file |
diff |
annotate
|
Thu, 27 Jan 1994 17:01:10 +0100 |
nipkow |
id -> idt in type of @filter and @Alls
|
file |
diff |
annotate
|
Mon, 24 Jan 1994 15:59:02 +0100 |
nipkow |
added conj_assoc to HOL_ss
|
file |
diff |
annotate
|
Wed, 03 Nov 1993 19:02:17 +0100 |
nipkow |
added append "@"
|
file |
diff |
annotate
|
Thu, 16 Sep 1993 12:21:07 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|