src/HOL/Library/Countable.thy
changeset 33640 0d82107dc07a
parent 31992 f8aed98faae7
child 35374 af1c8c15340e
--- a/src/HOL/Library/Countable.thy	Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/Library/Countable.thy	Thu Nov 12 17:21:51 2009 +0100
@@ -165,7 +165,7 @@
 text {* Lists *}
 
 lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs"
-  by (simp add: comp_def map_compose [symmetric])
+  by (simp add: comp_def)
 
 primrec
   list_encode :: "'a\<Colon>countable list \<Rightarrow> nat"