author | wenzelm |
Wed, 14 Jun 2000 17:59:53 +0200 | |
changeset 9066 | b1e874e38dab |
parent 3842 | b55686a7b22c |
child 12919 | d6a0d168291e |
permissions | -rw-r--r-- |
(* Title: HOL/MiniML/Maybe.thy ID: $Id$ Author: Wolfgang Naraschewski and Tobias Nipkow Copyright 1996 TU Muenchen Universal error monad. *) Maybe = Option + List + constdefs option_bind :: ['a option, 'a => 'b option] => 'b option "option_bind m f == case m of None => None | Some r => f r" syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0) translations "P := E; F" == "option_bind E (%P. F)" end