src/HOL/MiniML/Maybe.thy
author wenzelm
Thu, 21 Feb 2002 20:09:19 +0100
changeset 12919 d6a0d168291e
parent 3842 b55686a7b22c
child 14422 b8da5f258b04
permissions -rw-r--r--
removed theory Option;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     1
(* Title:     HOL/MiniML/Maybe.thy
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     2
   ID:        $Id$
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
     4
   Copyright  1996 TU Muenchen
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     5
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     6
Universal error monad.
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     7
*)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     8
12919
d6a0d168291e removed theory Option;
wenzelm
parents: 3842
diff changeset
     9
Maybe = Main +
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    10
1557
fe30812f5b5e added constdefs section
clasohm
parents: 1400
diff changeset
    11
constdefs
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
    12
  option_bind :: ['a option, 'a => 'b option] => 'b option
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
    13
  "option_bind m f == case m of None => None | Some r => f r"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    14
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1557
diff changeset
    15
syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0)
3842
b55686a7b22c fixed dots;
wenzelm
parents: 2525
diff changeset
    16
translations "P := E; F" == "option_bind E (%P. F)"
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1376
diff changeset
    17
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    18
end