| Thu, 25 Aug 1994 11:01:45 +0200 |
lcp |
INSTALLATION OF INDUCTIVE DEFINITIONS
|
file |
diff |
annotate
|
| Thu, 18 Aug 1994 12:07:51 +0200 |
lcp |
HOL/Nat: rotated arguments of nat_case; added translation for case macro
|
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
|
| Fri, 24 Jun 1994 15:11:39 +0200 |
lcp |
HOL/Nat/less_asym: renamed from less_anti_sym
|
file |
diff |
annotate
|
| Tue, 22 Mar 1994 08:31:58 +0100 |
nipkow |
Updated simpsets and a few proofs.
|
file |
diff |
annotate
|
| Wed, 16 Feb 1994 15:13:53 +0100 |
nipkow |
added more lemmas (also to nat_ss)
|
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, 29 Nov 1993 18:35:02 +0100 |
nipkow |
changed simpsets
|
file |
diff |
annotate
|
| Thu, 07 Oct 1993 10:20:30 +0100 |
lcp |
added ~= for "not equals" and added ~: for "not in"
|
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
|