| Fri, 17 Mar 1995 15:48:55 +0100 |
nipkow |
Added a few thms to nat_ss and list_ss
|
file |
diff |
annotate
|
| Mon, 13 Feb 1995 15:12:08 +0100 |
nipkow |
Added "flat"
|
file |
diff |
annotate
|
| Wed, 08 Feb 1995 11:34:11 +0100 |
nipkow |
More rewrite rules.
|
file |
diff |
annotate
|
| Thu, 26 Jan 1995 10:41:21 +0100 |
nipkow |
Added "nth" and some lemmas.
|
file |
diff |
annotate
|
| Wed, 14 Dec 1994 11:17:18 +0100 |
clasohm |
added bind_thm for theorems made by "standard ..."
Isabelle94-2
|
file |
diff |
annotate
|
| Thu, 08 Dec 1994 12:50:38 +0100 |
clasohm |
replaced store_thm by bind_thm
|
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
|
| Mon, 21 Nov 1994 17:50:34 +0100 |
clasohm |
replaced 'val ... = result()' by 'qed "..."'
|
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
|
| Fri, 17 Jun 1994 18:30:18 +0200 |
lcp |
HOL/List/map_append,map_compose: new
|
file |
diff |
annotate
|
| Wed, 02 Mar 1994 12:26:55 +0100 |
clasohm |
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
|
file |
diff |
annotate
|
| Tue, 15 Feb 1994 10:05:17 +0100 |
nipkow |
deleted duplicate rewrite rules
|
file |
diff |
annotate
|
| Thu, 03 Feb 1994 09:55:47 +0100 |
nipkow |
Introduction of various new lemmas and of case_tac.
|
file |
diff |
annotate
|
| Mon, 24 Jan 1994 15:59:02 +0100 |
nipkow |
added conj_assoc to HOL_ss
|
file |
diff |
annotate
|
| Mon, 29 Nov 1993 18:35:02 +0100 |
nipkow |
changed simpsets
|
file |
diff |
annotate
|
| Wed, 03 Nov 1993 19:02:17 +0100 |
nipkow |
added append "@"
|
file |
diff |
annotate
|
| Thu, 07 Oct 1993 10:20:30 +0100 |
lcp |
added ~= for "not equals" and added ~: for "not in"
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:21:07 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|