src/HOL/Library/Permutations.thy
changeset 34102 d397496894c4
parent 33715 8cce3a34c122
child 36335 ceea7e15c04b
     1.1 --- a/src/HOL/Library/Permutations.thy	Wed Dec 16 14:38:35 2009 -0800
     1.2 +++ b/src/HOL/Library/Permutations.thy	Wed Dec 16 15:10:08 2009 -0800
     1.3 @@ -15,7 +15,6 @@
     1.4  (* Transpositions.                                                           *)
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  
     1.7 -declare swap_self[simp]
     1.8  lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
     1.9    by (auto simp add: expand_fun_eq swap_def fun_upd_def)
    1.10  lemma swap_id_refl: "Fun.swap a a id = id" by simp