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.
simplified proof
authorhaftmann
Tue, 23 Jun 2009 14:24:58 +0200
changeset 31776 151c3f5f28f9
parent 31775 2b04504fcb69
child 31777 f897fe880f9d
simplified proof
src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Jun 23 12:09:30 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Jun 23 14:24:58 2009 +0200
@@ -1204,10 +1204,6 @@
     apply simp
     unfolding One_nat_def[symmetric] natlist_trivial_1
     apply simp
-    unfolding image_Collect[symmetric]
-    unfolding Collect_def mem_def
-    apply (rule finite_imageI)
-    apply blast
     done
 qed
isabelle