Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/List.thy
changeset 50027 7747a9f4c358
parent 49963 326f87427719
child 50134 13211e07d931 
--- a/src/HOL/List.thy	Thu Nov 08 11:59:47 2012 +0100
+++ b/src/HOL/List.thy	Thu Nov 08 11:59:48 2012 +0100
@@ -4026,7 +4026,7 @@
  (is "finite ?S")
 proof-
   have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
-  thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
+  thus ?thesis by (auto intro!: finite_lists_length_eq[OF `finite A`] simp only:)
 qed
 
 lemma card_lists_length_le:
isabelle