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