src/HOL/ex/Perm.thy
changeset 1376 92f83b9d17e1
parent 1193 026221bc9b2d
child 1476 608483c2122a
     1.1 --- a/src/HOL/ex/Perm.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/ex/Perm.thy	Fri Dec 01 12:03:13 1995 +0100
     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] 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"