| author | nipkow |
| Fri Oct 09 11:16:04 1998 +0200 (1998-10-09) | |
| changeset 5628 | 15b7f12ad919 |
| child 6301 | 08245f5a436d |
| permissions | -rw-r--r-- |
| nipkow@5628 | 1 |
(* Title: HOL/Induct/Multiset0.ML |
| nipkow@5628 | 2 |
ID: $Id$ |
| nipkow@5628 | 3 |
Author: Tobias Nipkow |
| nipkow@5628 | 4 |
Copyright 1998 TUM |
| nipkow@5628 | 5 |
|
| nipkow@5628 | 6 |
This theory merely proves that the representation of multisets is nonempty. |
| nipkow@5628 | 7 |
*) |
| nipkow@5628 | 8 |
|
| nipkow@5628 | 9 |
Goal "(%x.0) : {f. finite {x. 0 < f x}}";
|
| nipkow@5628 | 10 |
by(Simp_tac 1); |
| nipkow@5628 | 11 |
qed "multiset_witness"; |