author | oheimb |
Tue, 04 Nov 1997 20:48:38 +0100 | |
changeset 4133 | 0a08c2b9b1ed |
parent 2019 | b45d9f2042e0 |
child 4192 | c38ab5af38b5 |
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)" end