1 (* Title: HOL/Induct/Multiset0.ML
2 ID: $Id$
3 Author: Tobias Nipkow
4 Copyright 1998 TUM
5
6 This theory merely proves that the representation of multisets is nonempty.
7 *)
8
9 Goal "(%x.0) : {f. finite {x. 0 < f x}}";
10 by(Simp_tac 1);
11 qed "multiset_witness";