src/HOL/MiniML/Maybe.thy
changeset 1557 fe30812f5b5e
parent 1400 5d909faf0e04
child 2525 477c05586286
     1.1 --- a/src/HOL/MiniML/Maybe.thy	Wed Mar 06 14:12:24 1996 +0100
     1.2 +++ b/src/HOL/MiniML/Maybe.thy	Wed Mar 06 14:19:39 1996 +0100
     1.3 @@ -10,10 +10,9 @@
     1.4  
     1.5  datatype 'a maybe =  Ok 'a | Fail
     1.6  
     1.7 -consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
     1.8 -
     1.9 -defs
    1.10 -  bind_def "m bind f == case m of Ok r => f r | Fail => Fail"
    1.11 +constdefs
    1.12 +  bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
    1.13 +  "m bind f == case m of Ok r => f r | Fail => Fail"
    1.14  
    1.15  syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
    1.16  translations "P := E; F" == "E bind (%P.F)"