option to export standardized proof terms (not scalable);

more kinds, notably for Isabelle/MMT;

refined proof of concept for bit operations

more lemmas

Clean: consolidate ROOT file for new session directories

merge from afp-2019

New entry Aristotles_Assertoric_Syllogistic

Website for Clean

New entry: Clean

Sigma_Commit_Crypto website

New entry Sigma_Commit_Crypto

merged

export toplevel proof similar to named PThm;

tuned signature;

proper protocol_message for bootstrap proofs;

proper export of bootstrap proofs (amending a6304b4664b6);

more robust -- avoid interference with Proofterm.proofs := 0 in ML_Bootstrap.

proper treatment of self thm_id;

added quickcheck setup

generalized

moved quickcheck setup to distribution

moved generic instance to distribution

moved quickcheck setup to distribution

moved generic instance to distribution

clarified signature: support partial read_proof to accommodate proof term…

turn hidden terms into dummy, e.g. relevant for boundary cases of…

support dummy term;

tuned signature;

proof boxes based on proof digest (not proof term): thus it works with…

proper Thm.transfer;

clarified files;

clarified proof_boxes (requires prune_proofs=false);

tuned;

more robust;

more robust: avoid looping Lazy.force due to misinterpreted interrupt;

more informative combination_proof, e.g. relevant for proper type inference in…

tuned -- more stable type inference;

updated to jdk-11.0.4+11;

updated to scala-2.12.10;

more support for proof terms;

more support for proof terms;

support for proof terms;

clarified proof export;

set_preproc for object-logics with type classes;

tuned signature;

skip (somewhat pointless) shrink_proof more uniformly;

apply_preproc for all proof boxes;

cumulative errors for session partitions;

proper guard for process_theory: ensure uniform precedence of results;

load HOL-Proofs first: it introduces some extra "thm" items that are required…

recovered proofs;

clarified count_file;

clarified modules;

more complete coverage of sessions: process_theory operation needs to handle…

proper build_graph to make session selection work as in "isabelle build";

clarified options;

incorporate sessions with record_proofs;

clarified signature;

clarified signature;

clarified signature;

clarified signature;

clarified "isabelle update" options -- more like "isabelle dump";

clarified treatment of base logic image;

simplified options: always split;

split into standard partitions, for improved scalability;

proper guard -- avoid bad result;

clarified defaults;

tuned signature;

clarified signature: static Dump.Context vs. dynamic Dump.Session;

made NBA translation explicit

tuned signature;

tuned signature;

clarified sessions/directories;

clarified signature default;

clarified signature default;

more operations for type classes;

setup preprocessing for HOL proofs;

support preprocessing of exported proofs;

early setup of proof preprocessing;

adapted to ML version;

clarified output and input of Typ/Term;

more compact XML;

more compact XML: separate environment for free variables;

more compact XML;

proper ML names;

clarified standard_proof_of: prefer expand_proof over somewhat adhoc…

merged

some treatment of OfClass proofs;

tuned signature;

proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g.

misc tuning and clarification;

clarified oracle_proof;

tuned;

tuned;

clarified signature;

tuned;

more compact XML representation;

tuned signature;

tuned;

proper generalize_proof: schematic variables need to be explicit in the…