beautified spacing for binders with symbols syntax, analogous to HOL.thy
(* Title: HOL/Induct/Multiset0.thy ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUMThis theory merely proves that the representation of multisets is nonempty.*)Multiset0 = Main