Corrected mixfix declaration of @perm
authorlcp
Tue, 25 Jul 1995 17:02:34 +0200
changeset 1193 026221bc9b2d
parent 1192 d3a3cae80f08
child 1194 563ecd14c1d8
Corrected mixfix declaration of @perm
src/HOL/ex/Perm.thy
--- a/src/HOL/ex/Perm.thy	Tue Jul 25 17:02:03 1995 +0200
+++ b/src/HOL/ex/Perm.thy	Tue Jul 25 17:02:34 1995 +0200
@@ -9,7 +9,7 @@
 Perm = List +
 
 consts  perm    :: "('a list * 'a list) set"   
-syntax "@perm"  :: "['a list, 'a list] => bool" ("_ <~~> _"  [50] 50)
+syntax "@perm"  :: "['a list, 'a list] => bool" ("_ <~~> _"  [50,50] 50)
 
 translations
     "x <~~> y" == "(x,y) : perm"