diff -r 21055ac27708 -r d549f2534e6d src/HOL/Induct/Multiset0.thy
--- a/src/HOL/Induct/Multiset0.thy	Wed Oct 18 23:35:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(*  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