changeset 34102 | d397496894c4 |
parent 33715 | 8cce3a34c122 |
child 36335 | ceea7e15c04b |
--- 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