author | lcp |
Tue, 25 Jul 1995 17:02:34 +0200 | |
changeset 1193 | 026221bc9b2d |
parent 1192 | d3a3cae80f08 |
child 1194 | 563ecd14c1d8 |
--- 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"