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;

more millisecond cleanup

updated documentation

try "smt" as a fallback for ATPs if "metis" fails/times out

more detailed preplay output

tuning

tuning

more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;

tuned;

merged