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".
nipkow@1300
     1
(* Title:     HOL/MiniML/Maybe.thy
nipkow@1300
     2
   ID:        $Id$
nipkow@2525
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
nipkow@2525
     4
   Copyright  1996 TU Muenchen
nipkow@1300
     5
nipkow@1300
     6
Universal error monad.
nipkow@1300
     7
*)
nipkow@1300
     8
nipkow@2525
     9
Maybe = Option + List +
nipkow@1300
    10
clasohm@1557
    11
constdefs
nipkow@2525
    12
  option_bind :: ['a option, 'a => 'b option] => 'b option
nipkow@2525
    13
  "option_bind m f == case m of None => None | Some r => f r"
nipkow@1300
    14
nipkow@2525
    15
syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0)
nipkow@2525
    16
translations "P := E; F" == "option_bind E (%P.F)"
nipkow@1400
    17
nipkow@1300
    18
end