1 (* Title: HOL/Induct/Multiset0.thy
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 Multiset0 = Main