author | clasohm |
Mon, 05 Feb 1996 21:29:06 +0100 | |
changeset 1476 | 608483c2122a |
parent 1400 | 5d909faf0e04 |
child 1557 | fe30812f5b5e |
permissions | -rw-r--r-- |
(* Title: HOL/MiniML/Maybe.thy ID: $Id$ Author: Dieter Nazareth and Tobias Nipkow Copyright 1995 TU Muenchen Universal error monad. *) Maybe = List + datatype 'a maybe = Ok 'a | Fail consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60) defs bind_def "m bind f == case m of Ok r => f r | Fail => Fail" syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0) translations "P := E; F" == "E bind (%P.F)" end