src/HOL/Library/Extended_Nat.thy
changeset 44890 22f665a2e91c
parent 44019 ee784502aed5
child 45539 787a1a097465
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -487,7 +487,7 @@
     1.4  proof (rule finite_subset)
     1.5    show "finite (enat ` {..n})" by blast
     1.6  
     1.7 -  have "A \<subseteq> {..enat n}" using le_fin by fastsimp
     1.8 +  have "A \<subseteq> {..enat n}" using le_fin by fastforce
     1.9    also have "\<dots> \<subseteq> enat ` {..n}"
    1.10      by (rule subsetI) (case_tac x, auto)
    1.11    finally show "A \<subseteq> enat ` {..n}" .