src/Tools/Haskell/Library.hs

 
 Basic library of Isabelle idioms.
 -}
 
 module Isabelle.Library
-  ((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line)
+  ((|>), (|->), (#>), (#->), the_default, fold, fold_rev, single, quote, trim_line)
 where
+
+import Data.Maybe
+
 
 {- functions -}
 
 (|>) :: a -> (a -> b) -> b
 x |> f = f x

 (#>) :: (a -> b) -> (b -> c) -> a -> c
 (f #> g) x = x |> f |> g
 
 (#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
 (f #-> g) x  = x |> f |-> g
+
+
+{- options -}
+
+the_default :: a -> Maybe a -> a
+the_default x Nothing = x
+the_default _ (Just y) = y
 
 
 {- lists -}
 
 fold :: (a -> b -> b) -> [a] -> b -> b