misc tuning;

move mono_neutral_cong from AFP/Deep_Learning/PP_Auxiliary

added veriT preprocessing proof reconstruction example

tuned proof

renaming

added is_empty

misc tuning and modernization;

tuned

merged

tuned

Merged

Simplified Gamma_Function

proper priority queue spec

misc tuning and modernization;

added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;

tuned proofs;

tuned proof;

tuned whitespace;

Added new / improved tactics for fields and rings

Corrected type of dummy pattern

split balance into two, clearer etc

ML antiquotation for generated computations

tuned

tuned structure and terminology

tuned scope of lazy computation

tuned data structure

dropped dead code

tuned name

removed unclear clause; slower but clearer

removed contribution by Daniel Stuewe, too detailed.

added concise log height bound lemma

updated package;

tuned;

tuned

dropped dead code

ensure no duplicates after preprocessing

reject polymorphic result types; formally generalized to multiple result types

explicit a-priori detection of unsuitable terms for computations

more options;

tuned;

experimental computations: use arbitrary generated code for RHSs, not just constants

tuned documentation

merged

updated to jdk-8u121;

clarified owner;

insist in proper GNU tar, to avoid subtle semantic differences;

hardlink within JVM; clarified file attributes;

tuned;

clarified operation: include dirs as well;

tuned;

tuned;

build_jdk in Scala;

corrected static scope: multi-argument composition does not apply partially

less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic

tuned;

added postorder

tuned

int version slicker

tuned

tuned

clarified theory name; tuned;

New material from Bertrand's postulate (file Bertrand_Discrete_Sqrt), and tidied an old messy proof

tuned

removed some old ASCII syntax;

prefer context groups;

misc tuning and modernization;

prefer context groups;

more symbols;

misc tuning and modernization;

isabelle update_cartouches -c -t;

more symbols via abbrevs;

tuned signature;

clarified classical rules;

misc tuning and updates according to Curry-Club Dec-2016;

added option -n, e.g. useful to generate Dockerfile only;

support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);

tuned -- nicer generated bash source;

afford approx. 10MB for curl, e.g. required for "isabelle components";

updated to jvm-1.8;

uniform use of ISABELLE_SCALAC_OPTIONS for scalac, notably for -Xmax-classfile-name on encrypted or docker file-systems;

clarified settings;

clarified signature: packages may be accessed in Isabelle/Scala;

tuned whitespace;

clarified packages (for z3);

proper tag syntax;

clarified packages; tuned message;

clarified packages;

more options;

do avoid suspicious Unicode;

more standard header; avoid suspicious Unicode;

build docker image from Isabelle application bundle for Linux;

tuned message;

Added Circle_Area to HOL-Analysis examples

tuned/minimized

added lemma

tuned whitespace;

more robust: delay switches thread context from timer to GUI and may get out of sync with revoke operation;

tuned signature;

tuned signature;

improved chart plotting

augmented user aliasses

proper treatment of utf-8

tuned;

support for semantic completion;

generalized types in lemmas

updated package;

enable vscode_unicode_symbols by default, despite asymmetry of input and output;

more documentation;

generated configuration for Prettify Symbols Mode;

tuned;

clarified text output wrt. symbols;

merged

tuned signature;

support "purge" operation on document model;

proper template;

tuned;

accomodate very big file_models and changed_files;

tuned;

tuned

separate instance for semidom_modulo