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