misc tuning and simplification;

misc tuning;

tuned signature; tuned;

quickcheck invocations in mutabelle must not catch codegenerator errors internally

sort assignment before simultaneous term_check, not isolated parse_term; prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment; simplified Syntax_Phases.decode_sort/decode_typ; discontinued unused Proof_Context.check_tvar;

tuned;

avoid inconsistent sort constraints;

localized Record.decode_type: use standard Proof_Context.get_sort; clarified Record.varifyT: more convential use of maxidx + 1;

tuned signature -- emphasize internal role of these operations;

proper configuration option; tuned;

tuned layout;

more precise messages with the tester's name in quickcheck; tuned

quickcheck fails with code generator errors only if one tester is invoked

removing extra arguments

removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result

tuned

more fragments to export, removed the one from Com

updated functor Named_Thms; updated type attribute;

disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;

entity markup for bound variables;

merged

made SML/NJ happy

adding some documentation about the values command to the isar reference

adding a minimal documentation about the code_pred command to the isar reference

more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);

clarified Local_Defs.export: avoid costly still_fixed test, return all defs;

eliminated obsolete tuning (NB: Thm.eta_conversion/Envir.eta_contract based on Same.operation);

tuned;