author | paulson |
Tue, 01 Oct 1996 17:44:54 +0200 | |
changeset 2051 | 067bf19a71b7 |
parent 1557 | fe30812f5b5e |
child 2525 | 477c05586286 |
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 constdefs bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60) "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