src/HOL/Library/Infinite_Set.thy
changeset 44890 22f665a2e91c
parent 44454 6f28f96a09bf
child 46783 3e89a5cab8d7
     1.1 --- a/src/HOL/Library/Infinite_Set.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Library/Infinite_Set.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -544,7 +544,7 @@
     1.4  
     1.5  lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
     1.6  apply (induct n arbitrary: S)
     1.7 - apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
     1.8 + apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
     1.9  apply simp
    1.10  apply (metis DiffE infinite_remove)
    1.11  done