Records:
- Record types are now by default printed with their type abbreviation
instead of the list of all field types. This can be configured via
the reference "print_record_type_abbr".
- Simproc "record_upd_simproc" for simplification of multiple updates
added (not enabled by default).
- Tactic "record_split_simp_tac" to split and simplify records added.
- Bug-fix and optimisation of "record_simproc".
- "record_simproc" and "record_upd_simproc" are now sensitive to
quick_and_dirty flag.
(* Title: HOL/MiniML/Maybe.thy
ID: $Id$
Author: Wolfgang Naraschewski and Tobias Nipkow
Copyright 1996 TU Muenchen
Universal error monad.
*)
Maybe = Main +
constdefs
option_bind :: ['a option, 'a => 'b option] => 'b option
"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)"
end