changeset 10258 | d549f2534e6d |
parent 10257 | 21055ac27708 |
child 10259 | 93ec82d535f2 |
--- 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