properly overwrite replay data from one compression iteration to another

tuning

merged;

unused;

more formal markup;

clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead; fewer squiggles;

just error, not a failed attempt to raise an exception;

tuned whitespace;

tuned;

generate comments in Isar proofs

allow merging of steps with subproofs

renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover

tuned behavior of 'smt' option

keep all proof methods in data structure until the end, to enhance debugging output

proper fresh name generation

code generation: explicitly declared identifiers gain predence over implicit ones

tuned

tuned storage of code identifiers

searchable underscores

added new option to documentation

added 'smt' option to control generation of 'by smt' proofs

renamed ML file

tuning

merged 'reconstructors' and 'proof methods'

added 'smt' as a proof method

when merging, don't try methods that failed or timed out for either of the steps for the combined step

tuning

refactor relabeling code

tuned data structure

tuned data structure

more flexible compression, choosing whichever proof method works

reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense

made SML/NJ happier

less aggressive evaluation

added a new version of 'metis' to the mix

implemented new 'try0_isar' semantics

tuning

better time slack, to account for ultra-quick proof methods

crucial fix: use right version of the step

more thorough, hybrid compression

tuning

got rid of 'try0' step that is now redundant

centralize more preplaying

tuning

centralize preplaying

tuned

fixed indentation

new lemmas involving phi from Lehmer AFP entry

more data structure rationalization

tuning

more data structure rationalization

rationalized threading of 'metis' arguments

refactored data structure (step 3)

refactoring of data structure (step 2)

'primitive' is not an adverb

unform treatment of preplay_timeout = 0 and > 0

refactor data structure (step 1)

tuned code

tuned factor

tuning

made SML/NJ happier

take intersection rather than union of methods when merging steps -- more efficient and natural

merge proof methods

use Skolem proof methods appropriately

simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods

reset timing information after changes

Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.

merged

proper config options; proper context for printing;

more standard file/module names;

Added material from Old_Number_Theory related to the Chinese Remainder Theorem

prefer top-down rewriting for output (i.e. uncheck), in accordance to term abbreviations (see 5d2fe4e09354) and AST translations;

proper context for printing;

more explicit low-level exception;

unused;

method_setup "lem";

lazy_pack is default context for ILL;

unused;

proper Simplifier method setup;

simplified sessions;

misc tuning and modernization;

version of Fermat's Theorem for type nat

merged

merged

include comment.sty 3.6 which still works with plain tex, in contrast to later 3.7 which is only for latex (slow due to file snippets) -- see also 30781cc78fc6;

generalized preplaying infrastructure to store various results for various methods

added a 'trace' option

tuning

moved code around

added 'algebra' to the mix

more informative trace

tuning

more concise Isar output

Restoring some proofs from the equivalent file in Old_Number_Theory.

better tracing + syntactically correct 'metis' calls

tuned ML function names

tuning

moved ML code around

tuned headers;

merge

compile

guarded against exception

tuning

refactor large ML file

use Local_Theory.define instead of Specification.definition for internal constants

compile

renamed many Sledgehammer ML files to clarify structure

renamed ML file

tuned comment

tuned ML file name

tuned ML file name

less hermetic tactics

merged

reverted unsound optimization

got rid of one of two Metis variants

tuning

unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer

killed needless pass

dependency reporting for code generation errors

more abstract dictionary construction