reused slice in Sledgehammer's minimizer

merged

A few trivial changes

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;

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

tuned --- accomodate scala3;

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

tuned --- fewer warnings in scala3;

tuned signature -- avoid warnings for scala3;

tuned -- avoid warnings for scala3;

removed unused flag (see 25c6423ec538);

clarified versions;

documentation on diagnostic devices for code generation

more correct language

Tweaks concerning the versions of Zhao's evolving lecture notes

Trying to simplify a bit more

enable an E option suggested by Petar Vukmirovic

More simplification of proofs. Removal of numeric references to Zhao.

tidying and simplification

merged

More purely cosmetic changes

used HTTPS for SystemOnTPTP

moved from AFP to distribution

tuned syntax

moved from AFP to distribution

simplified some proofs and deleted quite a bit of redundant material

avoid static access to sun.tools.jconsole: more robust compilation (notably…

clarified signature;

more operations;

Shorter proofs and leaner notation.

Minor updates supplied by the author, mostly connected with a reference to a…

tuned: avoid ambiguity in scala3;

clarified signature: avoid ambiguity in scala3;

clarified signature: avoid ambiguity in scala3;

tuned for scala3;

more robust types (for scala3);

proper indentation (relevant for scala3);

Add a construction, using ZFC_in_HOL, of the category of small sets and…

Resolve a "Duplicate constant declaration" issue that occurs with "isabelle…

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

avoid side effects on working copy while runnign sessions (generated code is…

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

clarified formatting, for the sake of scala3;

clarified formatting, for the sake of scala3;

merged

clarified formatting, for the sake of scala3;

tuned formatting;

tuned

tuned

Deleted a few redundant lines

Trying to beautify this, but it's still ugly

merge

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

merged

tuned sledgehammer documentation

merged

tuned spelling;

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…

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;

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

provide SCALA_INTERFACES for isabelle_setup;

added documentation

tuned sledehammer to return best succeeding preplay method

merged

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…

further tweaked E's setup

And a bit more tidying

more renaming and tidying

Alphabetic substitutions

tweaked E setup

Eliminated another finiteness assumption

Removal of some needless finiteness assumptions

Removed a small amount of redundant material from both Szemerédi and Roth

merged

post-merged into new Lethe code

merged

fixed generation of Isar proofs e89709b80b6e

NEWS and CONTRIBUTORS

nicer TPTP output

regenerated

tighter check to ensure that patterns remain left-linear, previous…

tuned

tuned

separated treatment of undefined bodys