| changeset 46448 | f1201fac7398 |
| parent 46440 | d4994e2e7364 |
| child 46500 | 0196966d6d2d |
--- a/src/HOL/List.thy Fri Feb 10 09:02:51 2012 +0100 +++ b/src/HOL/List.thy Fri Feb 10 09:47:59 2012 +0100 @@ -3372,7 +3372,7 @@ lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs" by (induct xs) auto -(* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat +(* Needs count:: 'a \<Rightarrow> 'a list \<Rightarrow> nat lemma length_removeAll: "length(removeAll x xs) = length xs - count x xs" *)