src/HOL/MiniML/Maybe.thy
author wenzelm
Fri Oct 10 19:02:28 1997 +0200 (1997-10-10)
changeset 3842 b55686a7b22c
parent 2525 477c05586286
child 12919 d6a0d168291e
permissions -rw-r--r--
fixed dots;
     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