changeset 67399 | eab6ce8368fa |
parent 65388 | a8d868477bc0 |
child 67730 | f91c437f6f68 |
--- a/src/HOL/Library/More_List.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Library/More_List.thy Wed Jan 10 15:25:09 2018 +0100 @@ -320,7 +320,7 @@ (simp add: strip_while_def length_dropWhile_le del: length_rev) lemma nth_default_strip_while_dflt [simp]: - "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs" + "nth_default dflt (strip_while ((=) dflt) xs) = nth_default dflt xs" by (induct xs rule: rev_induct) auto lemma nth_default_eq_iff: