# HG changeset patch
# User nipkow
# Date 1636471033 -3600
# Node ID 1d0d6a3a3eb93fb4d5dcd3d491c91e0b4ae6b2cc
# Parent  6e1fad4f602b106f55751a7f4d7db1e7f3497c7f
tuned attributes to avoid looping

diff -r 6e1fad4f602b -r 1d0d6a3a3eb9 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 08 19:56:15 2021 +0100
+++ b/src/HOL/List.thy	Tue Nov 09 16:17:13 2021 +0100
@@ -1241,7 +1241,7 @@
   qed
 qed simp
 
-lemma rev_eq_Cons_iff[simp]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
+lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
 by(rule rev_cases[of xs]) auto
 
 
@@ -2115,7 +2115,10 @@
 lemma take_all_iff [simp]: "take n xs = xs \<longleftrightarrow> length xs \<le> n"
 by (metis length_take min.order_iff take_all)
 
+(* Looks like a good simp rule but can cause looping;
+   too much interaction between take and length
 lemmas take_all_iff2[simp] = take_all_iff[THEN eq_iff_swap]
+*)
 
 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
   by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)