--- a/src/ZF/Perm.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Perm.thy Sat Dec 09 13:36:11 1995 +0100
@@ -11,9 +11,9 @@
Perm = ZF + "mono" +
consts
- O :: "[i,i]=>i" (infixr 60)
- id :: "i=>i"
- inj,surj,bij:: "[i,i]=>i"
+ O :: [i,i]=>i (infixr 60)
+ id :: i=>i
+ inj,surj,bij:: [i,i]=>i
defs