merged

indexed document

allow multiple registration of the same type, the last wins

fixed problem (?) by deleting "thm" line

try right bunch of methods

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;