src/HOL/List.thy
changeset 50027 7747a9f4c358
parent 49963 326f87427719
child 50134 13211e07d931
     1.1 --- a/src/HOL/List.thy	Thu Nov 08 11:59:47 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Nov 08 11:59:48 2012 +0100
     1.3 @@ -4026,7 +4026,7 @@
     1.4   (is "finite ?S")
     1.5  proof-
     1.6    have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
     1.7 -  thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
     1.8 +  thus ?thesis by (auto intro!: finite_lists_length_eq[OF `finite A`] simp only:)
     1.9  qed
    1.10  
    1.11  lemma card_lists_length_le: