| Fri, 17 Jan 1997 11:09:19 +0100 |
paulson |
New miniscoping rules for the bounded quantifiers and UN/INT operators
|
file |
diff |
annotate
|
| Mon, 07 Oct 1996 10:28:44 +0200 |
paulson |
Removed commands made redundant by new one-point rules
|
file |
diff |
annotate
|
| Tue, 24 Sep 1996 08:59:24 +0200 |
nipkow |
Moved Option into core HOL which caused a few local changes.
|
file |
diff |
annotate
|
| Thu, 05 Sep 1996 10:27:36 +0200 |
paulson |
Simplified some proofs for compatibility with miniscoping
|
file |
diff |
annotate
|
| Tue, 30 Jul 1996 17:33:26 +0200 |
berghofe |
Classical tactics now use default claset.
|
file |
diff |
annotate
|
| Fri, 28 Jun 1996 15:30:55 +0200 |
paulson |
Removed a use of eq_cs
|
file |
diff |
annotate
|
| Tue, 23 Apr 1996 16:58:57 +0200 |
oheimb |
repaired critical proofs depending on the order inside non-confluent SimpSets
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 13:12:14 +0100 |
clasohm |
added local simpsets
|
file |
diff |
annotate
|
| Thu, 13 Apr 1995 17:05:41 +0200 |
nipkow |
Olafs new version.
|
file |
diff |
annotate
|
| Fri, 24 Mar 1995 12:30:35 +0100 |
clasohm |
changed syntax of tuples from <..., ...> to (..., ...)
|
file |
diff |
annotate
|
| Mon, 20 Mar 1995 15:37:03 +0100 |
clasohm |
converted IOA with curried function application
|
file |
diff |
annotate
|