don't waste time with old-style 'case's that don't have the required theorems

expand 'split' in direct corecursion as well

tuning

adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas

merge

properly massage 'if's / 'case's etc. under lambdas

Merge

Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.

fixed handling of 'split'

made SML/NJ happy

agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention

more exception cleanup + more liberal compressions of steps that timed out

tuned code to avoid noncanonical (and risky) exception handling

got rid of indices

corrected wrong 'meth :: _' pattern maching + tuned code

more generous Isar proof compression -- try to remove failing steps

tweaked handling of 'hopeless' methods

do a second phase of proof compression after minimization

don't give up on hopeless proof methods -- they can become hopeful again

tuned code

tuned slack

split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)

removal of "back", etc.

Restoration of Pocklington.thy. Tidying.

tuned latex

tuned latex

tuned

started index

interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state

removed legacy 'metisFT' method

tuning

tuning

more liberal step merging

rationalized lists of methods

extended method list

don't lose additional outcomes

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