changeset 14706 | 71590b7733b7 |
parent 14691 | e1eedc8cad37 |
child 14722 | 8e739a6eaf11 |
--- a/src/HOL/Library/Multiset.thy Thu May 06 12:43:00 2004 +0200 +++ b/src/HOL/Library/Multiset.thy Thu May 06 14:14:18 2004 +0200 @@ -4,10 +4,7 @@ License: GPL (GNU GENERAL PUBLIC LICENSE) *) -header {* - \title{Multisets} - \author{Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson} -*} +header {* Multisets *} theory Multiset = Accessible_Part: