| Thu, 25 Aug 1994 11:01:45 +0200 |
lcp |
INSTALLATION OF INDUCTIVE DEFINITIONS
|
file |
diff |
annotate
|
| Thu, 18 Aug 1994 11:30:27 +0200 |
lcp |
HOL/LList: swapped args of split and simplified
|
file |
diff |
annotate
|
| Wed, 29 Jun 1994 12:04:04 +0200 |
clasohm |
added parentheses made necessary by change of constrain's precedence
|
file |
diff |
annotate
|
| Tue, 19 Apr 1994 10:50:00 +0200 |
nipkow |
changed defns in hol.thy from = to ==
|
file |
diff |
annotate
|
| Tue, 15 Feb 1994 10:05:17 +0100 |
nipkow |
deleted duplicate rewrite rules
|
file |
diff |
annotate
|
| Wed, 26 Jan 1994 17:53:27 +0100 |
nipkow |
sum: renamed case to sum_case
|
file |
diff |
annotate
|
| Wed, 22 Dec 1993 12:43:37 +0100 |
nipkow |
added Pair_eq to pair_ss in prod.ML
|
file |
diff |
annotate
|
| Wed, 01 Dec 1993 13:05:25 +0100 |
lcp |
HOL/llist/LList_corec_subset1: does not need induction
|
file |
diff |
annotate
|
| Wed, 22 Sep 1993 15:43:05 +0200 |
lcp |
Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:21:07 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|