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