removed rotten code;

more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example: lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))" using [[simp_depth_limit = 1]] apply simp oops

merged

improved lin.arith. for terms involving division

restoring ancient string_classes option

method names in instance declarations are always unqualified

dropped legacy finally

tidied messy proofs

minimal document;

removed junk;

merged

check scalable fonts;

do *not* enforce scalable fonts for T1 encoding, instead rely on cm-super fonts, which also provide underscore for non-tt font;

yet another attempt at actual underscore; enforce scalable fonts for T1 encoding;

build up preprocessing context only once

tuned

disabled counterexample output for now; confusing because often incorrect

more indexing

merged

indexed document

Simplified some proofs, deleting a lot of strange unused material at the end of the theory.

fight spurious nitpick timeouts

reverted a87e49f4336d -- overwriting of data entries yields to merge problems later

more docs

more docs

docs

tidied

docs

docs about registering a BNF

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;

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