src/HOL/Library/Enum.thy
changeset 33639 603320b93668
parent 33635 dcaada178c6f
child 37601 2a4fb776ca53
     1.1 --- a/src/HOL/Library/Enum.thy	Thu Nov 12 17:21:43 2009 +0100
     1.2 +++ b/src/HOL/Library/Enum.thy	Thu Nov 12 17:21:48 2009 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4    by (induct n) simp_all
     1.5  
     1.6  lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
     1.7 -  by (induct n) (auto simp add: length_concat map_compose [symmetric] o_def listsum_triv)
     1.8 +  by (induct n) (auto simp add: length_concat o_def listsum_triv)
     1.9  
    1.10  lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    1.11    by (induct n arbitrary: ys) auto
    1.12 @@ -246,7 +246,7 @@
    1.13      by (auto simp add: image_def)
    1.14    have "set (map set (sublists xs)) = Pow (set xs)"
    1.15      by (induct xs)
    1.16 -      (simp_all add: aux Let_def Pow_insert Un_commute)
    1.17 +      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
    1.18    then show ?thesis by simp
    1.19  qed
    1.20