| changeset 3842 | b55686a7b22c |
| parent 2525 | 477c05586286 |
| child 12919 | d6a0d168291e |
--- a/src/HOL/MiniML/Maybe.thy Fri Oct 10 18:37:49 1997 +0200 +++ b/src/HOL/MiniML/Maybe.thy Fri Oct 10 19:02:28 1997 +0200 @@ -13,6 +13,6 @@ "option_bind m f == case m of None => None | Some r => f r" syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0) -translations "P := E; F" == "option_bind E (%P.F)" +translations "P := E; F" == "option_bind E (%P. F)" end