src/HOL/Option.thy
author berghofe
Fri, 24 Jul 1998 13:03:20 +0200
changeset 5183 89f162de39cf
parent 4752 1c334bd00038
child 5445 3905974ad555
permissions -rw-r--r--
Adapted to new datatype package.

(*  Title:      Option.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1994  TU Muenchen

Datatype 'a option
*)

Option = Datatype +

datatype 'a option = None | Some 'a

constdefs

  the		:: "'a option => 'a"
 "the == %y. case y of None => arbitrary | Some x => x"

  option_map	:: "('a => 'b) => ('a option => 'b option)"
 "option_map == %f y. case y of None => None | Some x => Some (f x)"

consts

  o2s	   :: "'a option => 'a set"

primrec
 "o2s  None    = {}"
 "o2s (Some x) = {x}"

end