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;

tuned;

tweaked comment

made SML/NJ happy

merged;

added FIXME comment

avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals

revived Refute in Mutabelle

tuned;

more scalable zero_var_indexes, depending on canonical order within table;

more benchmarks;

try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways

replace higher-order matching against schematic theorem with dedicated reconstruction method

merged

tuned signature -- avoid spurious Thm.mixed_attribute;

discontinued numbered structure indexes (legacy feature);

tuned proofs;