| Fri, 17 Jan 1997 18:19:57 +0100 |
wenzelm |
addsimps, addeqcongs: replaced @ by gen_union;
|
changeset |
files
|
| Fri, 17 Jan 1997 16:58:59 +0100 |
nipkow |
Incorporated Larry's changes.
|
changeset |
files
|
| Fri, 17 Jan 1997 16:17:31 +0100 |
paulson |
New rewrites for bounded quantifiers
|
changeset |
files
|
| Fri, 17 Jan 1997 13:21:54 +0100 |
nipkow |
This is the old version og MiniML for the monomorphic case.
|
changeset |
files
|
| Fri, 17 Jan 1997 13:16:36 +0100 |
nipkow |
Modified some defs and shortened proofs.
|
changeset |
files
|
| Fri, 17 Jan 1997 12:49:31 +0100 |
paulson |
Now with Andy Gordon's treatment of freshness to replace newN/K
|
changeset |
files
|
| Fri, 17 Jan 1997 11:50:09 +0100 |
paulson |
Deleted the redundant theorem subset_empty_iff (subset_empty exists already)
|
changeset |
files
|
| Fri, 17 Jan 1997 11:13:18 +0100 |
paulson |
Added the prlim command
|
changeset |
files
|
| Fri, 17 Jan 1997 11:09:19 +0100 |
paulson |
New miniscoping rules for the bounded quantifiers and UN/INT operators
|
changeset |
files
|
| Fri, 17 Jan 1997 10:09:46 +0100 |
nipkow |
Got rid of Alls in List.
|
changeset |
files
|
| Fri, 17 Jan 1997 10:04:28 +0100 |
nipkow |
Got rid of Alls in favour of !x:set_of_list
|
changeset |
files
|
| Thu, 16 Jan 1997 16:53:15 +0100 |
wenzelm |
binary oprations and relations;
|
changeset |
files
|