src/HOL/Option.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9001 93af64f54bf2
permissions -rw-r--r--
hide many names from Datatype_Universe.

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

Datatype 'a option
*)

Option = Datatype +

datatype 'a option = None | Some 'a

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

primrec
 "the (Some x) = x"

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

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

end