added dummy_thf prover to Sledgehammer

fixed typo

simplified hierarchy of type classes for bit operations

simplified hierarchy of type classes for bit operations

obsolete

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

restored executable conversions

dropped junk

more operations on types and terms;

clarified jEdit java sources;

clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for…

removed junk;

moved theory Bit_Operations into Main corpus

moved theory Bit_Operations into Main corpus

more operations;

clarified signature;

clarified signature;

organize syntax for word operations in bundles

organize syntax for word operations in bundles

support for Lazy.Text;

prefer compact Isabelle.Bytes;

clarified signature;

clarified signature --- more operations;

clarified order of modules;

tuned;

more operations;

tuned;

more systematic approach for instantiation

avoid seemingly unused transfer rules

clarified signature;

tuned signature;

clarified signature;

merged

tuned;

prefer Isabelle.Bytes, based on ShortByteString;

tuned signature: more generic operations;

tuned signature;

prefer UTF8 implementation from Data.Text.Encoding (foreign C);

cleaner presentation of analysis theorems in preliminaries

Update to new Epistemic_Logic.thy

Avoid typedefs

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

fixed TFX generation when universal quantifier is used as term

merged

merged

support for native symlinks on Windows;

various improvements of "isabelle scala_project";

tuned Mirabelle's theory selection

Clean: set AFP standard document options

Clean: re-add to chapter AFP

merge from afp-2021

Finitely_Generated_Abelian_Groups website

new entry Finitely_Generated_Abelian_Groups

Added Finitely_Generated_Abelian_Groups to metadata

clarified signature;

clarified signature;

updated for Isabelle2021 release;

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

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

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

clarified compiler output: allow multithreaded execution;

clarified signature;

clarified signature: more operations;

clarified props: more permissive;

clarified properties: "module" and "no_build";

more robust;

clarified signature;

clarified signature;

tuned comments;

tuned document;

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

Sync with my development repo. Add new material: "concrete bicategories" and

added simp_options to meson

parse TPTP operator @ also when not parenthesized

tuning

tuned E's lambda encoding

removed setup for outdated CVC3 from Isabelle

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

updated Sledgehammer docs -- removed most version numbers since these are…

compile

tuned;

NEWS;

updated documentation on Isabelle/Scala;

clarified component setup: exclude jar from active component, but use sources…

discontinued obsolete Apple (deprecated);

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…

more portable across history;

proper isabelle.setup.Setup build;

rebuild component;

more complete scala_project, including Isabelle/jEdit plugins;

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

clarified directories;

tuned;