sort assignment before simultaneous term_check, not isolated parse_term; prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment; simplified Syntax_Phases.decode_sort/decode_typ; discontinued unused Proof_Context.check_tvar;

tuned;

avoid inconsistent sort constraints;

localized Record.decode_type: use standard Proof_Context.get_sort; clarified Record.varifyT: more convential use of maxidx + 1;

tuned signature -- emphasize internal role of these operations;

proper configuration option; tuned;

tuned layout;

more precise messages with the tester's name in quickcheck; tuned

quickcheck fails with code generator errors only if one tester is invoked

removing extra arguments

removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result

tuned

more fragments to export, removed the one from Com

updated functor Named_Thms; updated type attribute;

disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;

entity markup for bound variables;

merged

made SML/NJ happy

adding some documentation about the values command to the isar reference

adding a minimal documentation about the code_pred command to the isar reference

more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);

clarified Local_Defs.export: avoid costly still_fixed test, return all defs;

eliminated obsolete tuning (NB: Thm.eta_conversion/Envir.eta_contract based on Same.operation);

tuned;

tuned;

tweaked comment

made SML/NJ happy

merged;

added FIXME comment

avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals

revived Refute in Mutabelle

tuned;

more scalable zero_var_indexes, depending on canonical order within table;

more benchmarks;

try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways

replace higher-order matching against schematic theorem with dedicated reconstruction method

merged

tuned signature -- avoid spurious Thm.mixed_attribute;

discontinued numbered structure indexes (legacy feature);

tuned proofs;

return outcome code, so that it can be picked up by Mutabelle

align columns in output and keep error log around

offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;

clarified attribute "mono_set": pure declaration, proper export in ML;

misc tuning;

made SML/NJ happy;

more millisecond cleanup

updated documentation

try "smt" as a fallback for ATPs if "metis" fails/times out

more detailed preplay output

tuning

tuning

more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;

tuned;

merged

cascading timeouts in minimizer, part 2

tuning

use "Time.time" rather than milliseconds internally

tune: no need for option

cascading timeouts in minimizer

shortcut binary minimization algorithm

speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half

renamed experimental systems

repaired quantification over type variables for non-TFF1/THF encodings

misc tuning and modernization; more antiquotations;

misc tuning and modernization; more antiquotations;

tuned;

some statespace benchmarks;

write changed .prv files only, to avoid writing into src file-space by default;

tuned document; tuned proofs;

more precise dependencies;

inlined antiquotations;

misc tuning and modernization;

optional timing, to avoid redundant allocation of mutable cells;

tuned;

misc tuning;

merged

more use of global operations (see 98ec8b51af9c)

more uniform instT_subst vs. inst_subst: compare variable names only;

tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;

misc tuning and modernization;

some performance tuning via Term_Subst/Same.operation; tuned;

pruned signature;

added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types; tuned;

more conventional syntax const;

proper syntactic category for abstraction syntax, to avoid low-level exception for malformed "\<integral> x y. f \<partial>M", for example;

merged

prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);

document new experimental provers

added remote iProver(-Eq) for experimentation

merged

ex/Tree23.thy: automate proof of gfull_add

ex/Tree23.thy: simplify proof of bal_del0

ex/Tree23.thy: simplify proof of bal_add0

ex/Tree23.thy: simpler definition of ordered-ness predicate

ex/Tree23.thy: prove that deletion preserves balance

more liberal Parse.fixes, to avoid overlap of mixfix with is-pattern (notably in 'obtain' syntax);

more general Proof_Context.bind_propp, which allows outer parameters; obtain: some support for term bindings within the proof, depending on parameters;

tuned whitespace;

tuned signature;

tuned signature -- canonical argument order;

tuned -- Variable.declare_term is already part of Variable.auto_fixes;

ex/Tree23.thy: prove that insertion preserves tree balance and order

more IMP fragments

string -> vname

JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.

more IMP text fragments

moved latex generation for HOL-IMP out of distribution

renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)

merged

more robust, declarative and unsurprising computation of types in the quotient type definition

improve handling of bound type variables (esp. for TFF1)