2010-08-01 bulwahn adding parsing of numbers; improving output of solution without free variables in prolog code generation
2010-08-01 bulwahn adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
2010-08-01 bulwahn adding basic arithmetic support for prolog code generation
2010-08-01 bulwahn adding numbers as basic term in prolog code generation
2010-07-31 ballarin More consistent naming of locale api functions.
2010-07-31 ballarin Documentation of 'interpret' updated.
2010-07-31 ballarin print_interps shows interpretations in proofs.
2010-07-31 ballarin Interpretation in proofs supports mixins.
2010-07-31 ballarin Make registrations generic data.
2010-07-30 blanchet merged
2010-07-29 blanchet don't choke on synonyms when parsing SPASS's Flotter output + renamings;
2010-07-29 blanchet fix Mirabelle timeout
2010-07-29 blanchet make Mirabelle happy
2010-07-29 blanchet fix bug in the newly introduced "bound concealing" code
2010-07-29 blanchet handle division by zero gracefully (used to raise Unordered later on)
2010-07-29 blanchet use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
2010-07-29 blanchet fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
2010-07-29 blanchet handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
2010-07-29 blanchet revert exception throwing in FOL_SOLVE, since they're not caught anyway
2010-07-29 blanchet avoid "ATP Error: Error: blah" style messages
2010-07-29 blanchet avoid "_def_raw" theorems
2010-07-29 blanchet better error and minimizer output
2010-07-29 blanchet deal with chained facts more gracefully
2010-07-29 blanchet speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
2010-07-29 blanchet work around atomization failures
2010-07-29 blanchet fiddle with the fudge factors, to get similar results as before
2010-07-29 blanchet perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
2010-07-29 blanchet fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
2010-07-29 blanchet generate correct names for "$true" and "$false";
2010-07-29 blanchet don't assume canonical rule format
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip