author | oheimb |
Mon, 27 Apr 1998 19:29:19 +0200 | |
changeset 4836 | fc5773ae2790 |
parent 4752 | 1c334bd00038 |
child 5183 | 89f162de39cf |
permissions | -rw-r--r-- |
(* Title: Option.thy ID: $Id$ Author: Tobias Nipkow Copyright 1994 TU Muenchen Datatype 'a option *) Option = Arith + 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 option "o2s None = {}" "o2s (Some x) = {x}" end