added predicate totalp_on and abbreviation totalp

excluded dummy ATPs from Sledgehammer's default provers

redefined order.{,strict_}mono as abbreviations of monotone

move monotone from Complete_Partial_Order to Orderings

added lemmas mult{,p}_mono_strong

qualified name to fix integrable_cong ambiguity

Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas

Eliminated two unnecessary inductions

NEWS

added lemma image_mset_filter_mset_swap

merged

»nil« seems to be a reserved constructor word in PolyML

added lemmas filter_mset_cong{0,}

tidied auto / simp with null arguments

tuned signature;

provide Isabelle/Electron test;

tuned text;

tuned text;

Tidied up some super-messy proofs

added lemmas image_mset_image_mset_mem_multI and multp_image_mset_image_msetI

added lemma image_mset_image_mset_mem_multI from AFP/SuperCalc

Added a couple of obvious simprules

added lemma

tuned signature: avoid problems with scala3;

proper indentation;

merged

clarified management of interpreter threads: more generic; avoid interp.bind, which is unavailable in scala3;

clarified signature;

clarified signature;

clarified signature, based on hints by IntelliJ IDEA;

tuned signature;

more robust: avoid partiality;

tuned;

clarified signature;

clarified signature;

tuned --- avoid warnings in scala3;

clarified signature;

pass new option only to new version of E

merged

merged

revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;

merged

tuned --- avoid warnings in scala3;

tuned --- avoid redundant patterns;

avoid pattern-match warnings, notably in scala3;

proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;

tuned --- accomodate scala3;

proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;

back to more ambitious scala-3.1.1 (see 8b7497992301);

tuned --- fewer warnings in scala3;

tuned -- avoid warnings for scala3;

tuned signature -- avoid warnings for scala3;

removed unused flag (see 25c6423ec538);

clarified versions;

documentation on diagnostic devices for code generation

more correct language

enable an E option suggested by Petar Vukmirovic

reused slice in Sledgehammer's minimizer

used HTTPS for SystemOnTPTP

moved from AFP to distribution

avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;

more operations; tuned message: Class.toString already says "class ...";

clarified signature;

tuned: avoid ambiguity in scala3;

clarified signature: avoid ambiguity in scala3;

clarified signature: avoid ambiguity in scala3;

more robust types (for scala3);

tuned for scala3;

proper indentation (relevant for scala3);

adjusted printing of type annotations to accomodate Scala 3

two new examples

pass constructor arity as part of case certficiate

tuned whitespace in generated code

tuned, centralizing case distinction at one place at the cost of modest duplication

clarified formatting, for the sake of scala3;

merged

tuned formatting;

clarified formatting, for the sake of scala3;

tuned

tuned

merge

tuned slices to get the fifth Zipperposition slice in a typical run

merged

tuned spelling;

merged

updated to scala-parser-combinators 2.1.0, which also fits to scala-3.0.2;

clarified invocation of isabelle.setup.Setup: -classpath allows multiple jars, as required for scala3;

tuned: eliminted do-while for the sake of scala3;

prefer scala 3.0.x, for option "-source 3.0-migration";

tuned: avoid problems with scala3;

tuned: avoid problems with scala3;

provide SCALA_INTERFACES for isabelle_setup;

build Isabelle Scala component from official downloads (for scala-3.1.1);

tuned sledgehammer documentation

added documentation

merged

further tweaked E's setup

tweaked E setup

merged

NEWS and CONTRIBUTORS

nicer TPTP output

tuned sledehammer to return best succeeding preplay method

expanded sledgehammer's expect option with some_preplayed

added preplay results to sledgehammer_output

tuned sledgehammer to suggest (smt (verit)) on failing smt preplay for all but Z3

expanded sledgehammer's expect option with some_preplayed

changed sledgehammer_output

post-merged into new Lethe code

merged

regenerated

tighter check to ensure that patterns remain left-linear, previous implementation was overcautious

tuned

tuned

separated treatment of undefined bodys

tuned arguments

modernized handling of variables

fixed generation of Isar proofs e89709b80b6e

fixed Sledgehammer generation of Isar proofs for SMT solvers broken by e89709b80b6e

structurally tuned

tuned names