src/HOL/MiniML/Maybe.thy
author nipkow
Fri Jan 17 18:50:04 1997 +0100 (1997-01-17)
changeset 2525 477c05586286
parent 1557 fe30812f5b5e
child 3842 b55686a7b22c
permissions -rw-r--r--
The new version of MiniML including "let".
     1 (* Title:     HOL/MiniML/Maybe.thy
     2    ID:        $Id$
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
     4    Copyright  1996 TU Muenchen
     5 
     6 Universal error monad.
     7 *)
     8 
     9 Maybe = Option + List +
    10 
    11 constdefs
    12   option_bind :: ['a option, 'a => 'b option] => 'b option
    13   "option_bind m f == case m of None => None | Some r => f r"
    14 
    15 syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0)
    16 translations "P := E; F" == "option_bind E (%P.F)"
    17 
    18 end