src/HOL/Option.thy
author berghofe
Tue May 30 18:02:49 2000 +0200 (2000-05-30)
changeset 9001 93af64f54bf2
parent 5445 3905974ad555
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
     1 (*  Title:      Option.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994  TU Muenchen
     5 
     6 Datatype 'a option
     7 *)
     8 
     9 Option = Datatype +
    10 
    11 datatype 'a option = None | Some 'a
    12 
    13 consts
    14   the :: "'a option => 'a"
    15   o2s :: "'a option => 'a set"
    16 
    17 primrec
    18  "the (Some x) = x"
    19 
    20 primrec
    21  "o2s  None    = {}"
    22  "o2s (Some x) = {x}"
    23 
    24 constdefs
    25   option_map	:: "('a => 'b) => ('a option => 'b option)"
    26  "option_map == %f y. case y of None => None | Some x => Some (f x)"
    27 
    28 end