Theory Option_Extra

theory Option_Extra ✐‹contributor ‹Balazs Toth›› 
  imports Main
begin

abbreviation get_or :: "'a option ⇒ 'a ⇒ 'a" where
  "⋀a default. get_or a default ≡ case a of None ⇒ default | Some a ⇒ a"

end