wenzelm [Fri, 17 Jan 1997 18:19:57 +0100] rev 2521
addsimps, addeqcongs: replaced @ by gen_union;
nipkow [Fri, 17 Jan 1997 16:58:59 +0100] rev 2520
Incorporated Larry's changes.
paulson [Fri, 17 Jan 1997 16:17:31 +0100] rev 2519
New rewrites for bounded quantifiers
nipkow [Fri, 17 Jan 1997 13:21:54 +0100] rev 2518
This is the old version og MiniML for the monomorphic case.
The new version is now in MiniML.
nipkow [Fri, 17 Jan 1997 13:16:36 +0100] rev 2517
Modified some defs and shortened proofs.
paulson [Fri, 17 Jan 1997 12:49:31 +0100] rev 2516
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson [Fri, 17 Jan 1997 11:50:09 +0100] rev 2515
Deleted the redundant theorem subset_empty_iff (subset_empty exists already)
paulson [Fri, 17 Jan 1997 11:13:18 +0100] rev 2514
Added the prlim command
paulson [Fri, 17 Jan 1997 11:09:19 +0100] rev 2513
New miniscoping rules for the bounded quantifiers and UN/INT operators
nipkow [Fri, 17 Jan 1997 10:09:46 +0100] rev 2512
Got rid of Alls in List.
Added Ball_insert and Ball_Un in equalities.ML.