changeset 21404 | eb85850d3eb7 |
parent 19380 | b808efaa5828 |
child 23755 | 1c4672d130b1 |
--- a/src/HOL/Library/Permutation.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Library/Permutation.thy Fri Nov 17 02:20:03 2006 +0100 @@ -12,7 +12,7 @@ perm :: "('a list * 'a list) set" abbreviation - perm_rel :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) + perm_rel :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) where "x <~~> y == (x, y) \<in> perm" inductive perm