author | berghofe |
Thu, 22 Dec 2005 13:31:58 +0100 | |
changeset 18491 | 1ce410ff9941 |
parent 18490 | 434e34392c40 |
child 18492 | b0fe60800623 |
--- a/src/HOL/Nominal/Nominal.thy Thu Dec 22 13:00:53 2005 +0100 +++ b/src/HOL/Nominal/Nominal.thy Thu Dec 22 13:31:58 2005 +0100 @@ -19,7 +19,7 @@ (* polymorphic operations for permutation and swapping*) consts - perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet> _" [80,80] 80) + perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<bullet>" 80) swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x" (* permutation on sets *)