src/HOL/List.thy

   have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)
   show ?case (is "?l = card ?S'")
   proof (cases)
     assume "p x"
     hence eq: "?S' = insert 0 (Suc ` ?S)"
-      by(auto simp: nth_Cons image_def split:nat.split dest:not0_implies_Suc)
+      by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
     have "length (filter p (x # xs)) = Suc(card ?S)"
       using Cons `p x` by simp
     also have "\<dots> = Suc(card(Suc ` ?S))" using fin
       by (simp add: card_image inj_Suc)
     also have "\<dots> = card ?S'" using eq fin
       by (simp add:card_insert_if) (simp add:image_def)
     finally show ?thesis .
   next
     assume "\<not> p x"
     hence eq: "?S' = Suc ` ?S"
-      by(auto simp add: image_def neq0_conv split:nat.split elim:lessE)
+      by(auto simp add: image_def split:nat.split elim:lessE)
     have "length (filter p (x # xs)) = card ?S"
       using Cons `\<not> p x` by simp
     also have "\<dots> = card(Suc ` ?S)" using fin
       by (simp add: card_image inj_Suc)
     also have "\<dots> = card ?S'" using eq fin

 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
 done
 
 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
 apply(induct xs arbitrary: I)
-apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: not0_implies_Suc)
+apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
 done
 
 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
 by(auto simp add:set_sublist)