# HG changeset patch
# User narboux
# Date 1175612752 -7200
# Node ID 2a1eef99bb6a2dbd75d124e9e9a925027969dce2
# Parent  98a290c4b0b4b7389b8eff86ae6935bb65cae8db
remove the lemma swap_fun which was not needed

diff -r 98a290c4b0b4 -r 2a1eef99bb6a src/HOL/Nominal/Nominal.thy
--- 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"
diff -r 98a290c4b0b4 -r 2a1eef99bb6a src/HOL/Nominal/nominal_permeq.ML
--- 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";