Tuned syntax for perm.
authorberghofe
Thu Dec 22 13:31:58 2005 +0100 (2005-12-22)
changeset 184911ce410ff9941
parent 18490 434e34392c40
child 18492 b0fe60800623
Tuned syntax for perm.
src/HOL/Nominal/Nominal.thy
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Dec 22 13:00:53 2005 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Dec 22 13:31:58 2005 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  (* polymorphic operations for permutation and swapping*)
     1.6  consts 
     1.7 -  perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     ("_ \<bullet> _" [80,80] 80)
     1.8 +  perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     (infixr "\<bullet>" 80)
     1.9    swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
    1.10  
    1.11  (* permutation on sets *)