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