Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
swap_self already declared [simp]
authorhuffman
Wed, 16 Dec 2009 15:10:08 -0800
changeset 34102 d397496894c4
parent 34101 d689f0b33047
child 34103 9095ba4d2cd4
swap_self already declared [simp]
src/HOL/Library/Permutations.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle