(* Title: HOL/Induct/Multiset0.thy ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM This theory merely proves that the representation of multisets is nonempty. *) Multiset0 = Main