replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset()
intro Introduction to Isabelle
ref The Isabelle Reference Manual
system The Isabelle System Manual
logics Isabelle's Object-Logics
ind-defs (Co)Inductive Definitions in ZF
axclass Tutorial on Axiomatic Type Classes