src/HOL/List.thy
changeset 51096 60e4b75fefe1
parent 50548 0aec55e63795
child 51112 da97167e03f7
     1.1 --- a/src/HOL/List.thy	Wed Feb 13 13:38:52 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Feb 13 13:38:52 2013 +0100
     1.3 @@ -162,6 +162,13 @@
     1.4  
     1.5  hide_const (open) find
     1.6  
     1.7 +primrec those :: "'a option list \<Rightarrow> 'a list option"
     1.8 +where
     1.9 +"those [] = Some []" |
    1.10 +"those (x # xs) = (case x of
    1.11 +  None \<Rightarrow> None
    1.12 +| Some y \<Rightarrow> Option.map (Cons y) (those xs))"
    1.13 +
    1.14  primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.15  "remove1 x [] = []" |
    1.16  "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"