--- a/src/HOL/Nominal/Nominal.thy Tue Apr 03 16:20:34 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Tue Apr 03 17:05:52 2007 +0200
@@ -81,10 +81,6 @@
defs (unchecked overloaded)
perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
-lemma swap_fun:
- shows "[(a,b)]\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. [(a,b)]\<bullet>f([(a,b)]\<bullet>x))"
-by (unfold perm_fun_def,auto)
-
(* permutation on bools *)
primrec (unchecked perm_bool)
true_eqvt: "pi\<bullet>True = True"