src/HOL/MiniML/Maybe.thy
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