Type inference bug in Isar attributes "where" and "of" fixed.

tidied

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.

Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by default.

fixed

set isatool usedir to verbose by default