adding some test cases for preprocessing and narrowing

adding a minimalistic preprocessing rewriting common boolean operators; tuned

merged

merged

tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1

use simproc_setup for some nat_numeral simprocs; add simproc tests

add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type s not in this class); test simprocs using most general type classes instead of just int and rat.

simultaneous check; tight maxidx;

avoid separate typ_check phases, integrate into main term_check 0 instead (cf. its Syntax.check_typs in Type_Infer_Context.prepare);

clarified singleton_fixate: intersection with supersort is identity, only replace actual type inference parameters; tuned reject_other, after_infer_fixate;

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;

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;

return outcome code, so that it can be picked up by Mutabelle

align columns in output and keep error log around

offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;

clarified attribute "mono_set": pure declaration, proper export in ML;

misc tuning;

made SML/NJ happy;