| changeset 1400 | 5d909faf0e04 |
| parent 1376 | 92f83b9d17e1 |
| child 1557 | fe30812f5b5e |
--- a/src/HOL/MiniML/Maybe.thy Fri Dec 08 13:22:55 1995 +0100 +++ b/src/HOL/MiniML/Maybe.thy Fri Dec 08 19:48:15 1995 +0100 @@ -15,4 +15,7 @@ defs bind_def "m bind f == case m of Ok r => f r | Fail => Fail" +syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0) +translations "P := E; F" == "E bind (%P.F)" + end