src/HOL/MiniML/Maybe.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 3842 b55686a7b22c
child 12919 d6a0d168291e
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
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)
wenzelm@3842
    16
translations "P := E; F" == "option_bind E (%P. F)"
nipkow@1400
    17
nipkow@1300
    18
end