more complete dockables;

more robust (see 4d91b6d5d49c);

avoid non-standard encoding;

tuned;

more robust;

more robust classpath: skip empty entries;

more robust: avoid duplicate classpath entries;

proper cross-platform build: jdk component is required for…

build.props for isabelle.jar, including isabelle.jedit;

more robust;

proper lines (amending 59b6f0462086);

more portable: avoid Windows CRLF in classpath output;

more systematic treatment of encodings;

tuned;

extended the 'corec' format slightly

Minor changes to Finitely_Generated_Abelian_Groups, simplified and extended…

new entry Finitely_Generated_Abelian_Groups

prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent

tuning

rephrase Nitpick constraint in more first-order format that's also more…

remove duplicate entry in metadata

correctly translate constructor argument in 'primrec'

simplified a few proofs

revisited ac28714b7478: more faithful preplaying with chained facts

added alternative E binary name

wait for E 2.7 before using 'ite' in HO mode

more coherent dependencies

fix(Regex_Equivalence) update to new SpecCheck version

parse logical operators in the right order w.r.t. backtracking

adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing)

improved warning

operations for symbolic computation of bit operations

proper local context

operations for symbolic computation of bit operations

fixed Proof_Strategy_Language following Isabelle/f58108b7a60c

shasum for project meta-info;

even more strict shasum (amending c9771e1b3223);

strict shasum: this is used on input files;

clarified Isabelle meta-info within jar;

clarified modules;

support for command-line operations;

operations for all components;

clarified signature;

merged

rebuild component;

expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;

skip scalac for Java build;

support expand_platform_path, which is reminiscent of isabelle.Path.expand;

support mixed Scala/Java build;

more robust;

clarified signature;

clarified syntax: similar to URL;

clarified javac options;

more compiler_deps via "requirements", notably jar list from settings;

more robust;

clarified component settings;

tuned signature;

clarified shasum: sources / resources within jar;

clarified modules;

merged

fixed HOL-TPTP following f58108b7a60c

documented Sledgehammer option "induction_rules"

promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"

refactored Sledgehammer option "induction_rules"

jenkins: add pre/post-hook results for benchmark

SpecCheck now without _ (Regex_Equivalence is still broken)

remove SpecCheck; it is now part of the AFP

merged from afp2021

T1 fontenc for new entries

new entry SpecCheck

update hide_lams -> opaque_lifting

sitegen

metadata and sitegen for MiniSail

website for SpecCheck

new entry: MiniSail

sitegen for Public Announcement Logic

new entry "Public Announcement Logic"

fixed a messy reference

Van_der_Waerden website

New entry IMP_Compiler

new entry Van_der_Waerden

Removal of unintended files

Hidden.thy to Isar

merged

added documentation for changes to Sledgehammer option "lam_trans"

merged

renamed hide_lams opaque_lifting

merged

jenkins: pre/post-hook results

jenkins: pre/post-hook results

changed to opaque_lifiting as suggested by Isabelle/Jenkins

changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins

merged

added opaque_combs and renamed hide_lams to opaque_lifting

more robust treatment of empty string;

invoke Scala compiler from Java, without external process;

Added missing Public_Announcement_Logic to ROOTS file

clarified version: Apple now counts like 11, 12, ...;

More Support on Clean Syntax, Basic Lens Support, New Examples.

finishing arg -> Arg and moving some material out of…