# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1643120013 0
# Node ID 43b3d5318d725ae7aad0206217f52fe44c3c7a6c
# Parent  2e16798b6f2bda7e4884086cabf0c3dc2e4c92c1
fixed dodgy intro! attributes

diff -r 2e16798b6f2b -r 43b3d5318d72 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Tue Jan 25 09:57:44 2022 +0100
+++ b/src/HOL/Library/More_List.thy	Tue Jan 25 14:13:33 2022 +0000
@@ -91,11 +91,11 @@
 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)
 
@@ -148,7 +148,7 @@
   "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