src/HOL/Library/Permutation.thy

--- a/src/HOL/Library/Permutation.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Library/Permutation.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -11,10 +11,9 @@
 consts
   perm :: "('a list * 'a list) set"
 
-syntax
-  "_perm" :: "'a list => 'a list => bool"    ("_ <~~> _"  [50, 50] 50)
-translations
-  "x <~~> y" == "(x, y) \<in> perm"
+abbreviation
+  perm_rel :: "'a list => 'a list => bool"    ("_ <~~> _"  [50, 50] 50)
+  "x <~~> y == (x, y) \<in> perm"
 
 inductive perm
   intros