# HG changeset patch
# User haftmann
# Date 1245759898 -7200
# Node ID 151c3f5f28f965bb70cfc12fc9d5a6c008bd8d14
# Parent  2b04504fcb690b38a26f9b8ee1a1fbeb2642f793
simplified proof

diff -r 2b04504fcb69 -r 151c3f5f28f9 src/HOL/Library/Formal_Power_Series.thy
--- 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