src/HOL/Library/More_List.thy

 
 definition no_leading :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
 where
   "no_leading P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (hd xs))"
 
-lemma no_leading_Nil [simp, intro!]:
+lemma no_leading_Nil [iff]:
   "no_leading P []"
   by (simp add: no_leading_def)
 
-lemma no_leading_Cons [simp, intro!]:
+lemma no_leading_Cons [iff]:
   "no_leading P (x # xs) \<longleftrightarrow> \<not> P x"
   by (simp add: no_leading_def)
 
 lemma no_leading_append [simp]:
   "no_leading P (xs @ ys) \<longleftrightarrow> no_leading P xs \<and> (xs = [] \<longrightarrow> no_leading P ys)"

 
 lemma no_trailing_unfold:
   "no_trailing P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (last xs))"
   by (induct xs) simp_all
 
-lemma no_trailing_Nil [simp, intro!]:
+lemma no_trailing_Nil [iff]:
   "no_trailing P []"
   by simp
 
 lemma no_trailing_Cons [simp]:
   "no_trailing P (x # xs) \<longleftrightarrow> no_trailing P xs \<and> (xs = [] \<longrightarrow> \<not> P x)"