added option labels to Mirabelle actions

more operations: dest binders;

clarified abstract and concrete boolean algebras

antiquotation for bundles

prefer persistent hash code for cachable items (see also 72b13af7f266);

merged

more operations: record overall exported entities;

merged

added dummy_fof prover to Sledgehammer

fixed malconfigured option output_dir in mirabelle

merged

clarified export of formal entities: name space info is always present, but content depends on option "export_theory";

proper name space "kind": this is a formal name, not comment;

more uniform signatures in ML and Scala;

merged

fixed typo

added dummy_thf prover to Sledgehammer

simplified hierarchy of type classes for bit operations

obsolete

more operations, notably free and bound variables as in Isabelle/Pure;

more operations on types and terms; abstract syntax operations for Pure and HOL;

clarified jEdit java sources;

clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for unknown reasons;

removed junk;

moved theory Bit_Operations into Main corpus

more operations;

clarified signature;

clarified signature;

organize syntax for word operations in bundles

support for Lazy.Text;

prefer compact Isabelle.Bytes;

clarified signature;

clarified signature --- more operations;

tuned;

clarified order of modules;

more operations;

tuned;

clarified signature;

tuned signature;

clarified signature;

merged

prefer Isabelle.Bytes, based on ShortByteString;

tuned;

tuned signature;

tuned signature: more generic operations;

prefer UTF8 implementation from Data.Text.Encoding (foreign C); clarified signatures and modules;

documented Mirabelle_Sledgehammer's new keep semantics

changed Mirabelle_Sledgehammer keep option from path to boolean

added automatic uniform stride option to Mirabelle

fixed HOL-ex following a5bab59d580b

added support for TFX $let to Sledgehammer's TPTP output

merged

fixed TFX generation when universal quantifier is used as term

merged

various improvements of "isabelle scala_project";

support for native symlinks on Windows;

tuned Mirabelle's theory selection

clarified signature;

clarified signature;

updated for Isabelle2021 release;

back to stackage lts-17.10, to make this work on vmnipkow9 (Windows Server 2012 R2);

update to Haskell stack-2.7.3 and stackage lts-17.15;

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

clarified signature;

clarified compiler output: allow multithreaded execution;

clarified signature: more operations;

clarified props: more permissive;

more robust;

clarified properties: "module" and "no_build"; clarified signature;

clarified signature;

clarified signature;

tuned comments;

tuned document;

clarified names (again), e.g. relevant for "Plugin Options";

added simp_options to meson

tuning

parse TPTP operator @ also when not parenthesized

removed setup for outdated CVC3 from Isabelle

tuned E's lambda encoding

use Vampire's clausifier with iProver, now that E's is no longer supported

updated Sledgehammer docs -- removed most version numbers since these are tedious to maintain

compile

tuned;

NEWS;

updated documentation on Isabelle/Scala;

discontinued obsolete Apple (deprecated);

clarified component setup: exclude jar from active component, but use sources from template within ISABELLE_HOME (relevant for "isabelle scala_project -L");

more robust "isabelle build_scala" as separate tool;

tuned --- based on hints by IntelliJ IDEA;

more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in AFP/1001c0dfced0);

more portable across history;

proper isabelle.setup.Setup build;

rebuild component;

more complete scala_project, including Isabelle/jEdit plugins;

clarified directories;

more accurate scala_project, based on build.props of components;

clarified build_props: empty module means no build; clarified signature; clarified errors;

tuned;

CONTRIBUTORS

merged

more robust;

rebuild component;

more robust: for the sake of Isabelle.app on macOS;

more robust;

more robust;

more robust;

rebuild component;

more informative errors: capture low-level compiler output;

more direct isabelle_scala_build: always enabled, no "Admin" requirement;

tuned --- fewer warnings;

clarified names;

tuned --- fewer warnings;

clarified directory;

clarified names;

clarified component setup for old graph browser;

redundant: *.class and *.jar are already ignored;

proper cat_lines: avoid last "\n";

merged

A few new lemmas and simplifications

removed support for experimental Pirate prover