--- a/src/ZF/Perm.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/ZF/Perm.thy Fri Jun 17 16:12:49 2005 +0200 @@ -11,7 +11,7 @@ header{*Injections, Surjections, Bijections, Composition*} -theory Perm = func: +theory Perm imports func begin constdefs