# HG changeset patch
# User huffman
# Date 1261005008 28800
# Node ID d397496894c4a3d5469a6cb4ad10d197cd6c0d04
# Parent  d689f0b3304718575726db796aaa457875802698
swap_self already declared [simp]

diff -r d689f0b33047 -r d397496894c4 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Wed Dec 16 14:38:35 2009 -0800
+++ b/src/HOL/Library/Permutations.thy	Wed Dec 16 15:10:08 2009 -0800
@@ -15,7 +15,6 @@
 (* Transpositions.                                                           *)
 (* ------------------------------------------------------------------------- *)
 
-declare swap_self[simp]
 lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
   by (auto simp add: expand_fun_eq swap_def fun_upd_def)
 lemma swap_id_refl: "Fun.swap a a id = id" by simp