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";