src/HOL/Library/Infinite_Set.thy
changeset 44454 6f28f96a09bf
parent 44169 bdcc11b2fdc8
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Library/Infinite_Set.thy	Mon Aug 22 16:49:45 2011 -0700
     1.2 +++ b/src/HOL/Library/Infinite_Set.thy	Mon Aug 22 17:22:49 2011 -0700
     1.3 @@ -546,7 +546,7 @@
     1.4  apply (induct n arbitrary: S)
     1.5   apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
     1.6  apply simp
     1.7 -apply (metis Collect_mem_eq DiffE infinite_remove)
     1.8 +apply (metis DiffE infinite_remove)
     1.9  done
    1.10  
    1.11  declare enumerate_0 [simp del] enumerate_Suc [simp del]