Corrected mixfix declaration of @perm
authorlcp
Tue Jul 25 17:02:34 1995 +0200 (1995-07-25 ago)
changeset 1193026221bc9b2d
parent 1192 d3a3cae80f08
child 1194 563ecd14c1d8
Corrected mixfix declaration of @perm
src/HOL/ex/Perm.thy
     1.1 --- a/src/HOL/ex/Perm.thy	Tue Jul 25 17:02:03 1995 +0200
     1.2 +++ b/src/HOL/ex/Perm.thy	Tue Jul 25 17:02:34 1995 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  Perm = List +
     1.5  
     1.6  consts  perm    :: "('a list * 'a list) set"   
     1.7 -syntax "@perm"  :: "['a list, 'a list] => bool" ("_ <~~> _"  [50] 50)
     1.8 +syntax "@perm"  :: "['a list, 'a list] => bool" ("_ <~~> _"  [50,50] 50)
     1.9  
    1.10  translations
    1.11      "x <~~> y" == "(x,y) : perm"