--- 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"
--- a/src/HOL/Nominal/nominal_permeq.ML Tue Apr 03 16:20:34 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Tue Apr 03 17:05:52 2007 +0200
@@ -54,7 +54,6 @@
val conj_absorb = thm "conj_absorb";
val not_false = thm "not_False_eq_True"
val perm_fun_def = thm "Nominal.perm_fun_def"
-val swap_fun = thm "Nominal.swap_fun" (* FIXME: is this still needed? *)
val perm_eq_app = thm "Nominal.pt_fun_app_eq"
val supports_def = thm "Nominal.op supports_def";
val fresh_def = thm "Nominal.fresh_def";