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

reduced prominence of "permissive code generation"

split rules for of_bool, similar to if

don't forget the last inference(s) after conjecture skolemization

centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)

keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized

renamed Sledgehammer options for symmetry between positive and negative versions

more robust w.r.t. exceptions raised by proof methods

tuning

compile