merge

increased timeout

collected combinatorial material

collected combinatorial material

tuned;

tuned;

more documentation;

proper treatment of nested antiquotations;

support for ML special forms: modified evaluation similar to Scheme;

clarified signature: more detailed token positions for antiquotations;

Update root.tex

Cut out Fitting's consistency properties

fixed proof

clarified message, following Isabelle/a7aabdf889b7;

merged

clarified signature;

confluent preprocessing for floats in presence of target language numerals

confluent preprocessing for floats in presence of target language numerals

subclass relation

subclass relation

some tinkering with npm versions;

some tinkering with npm versions;

back to post-release mode;

tuned signature;

tuned;

auto-update due to "isabelle build_vscode";

tuned --- following hints by IntelliJ IDEA;

fixed problematic addition operation in the 'approximation' package (previous…

adapted to isabelle-dev/56db8559eadb

simplified definition

simplified definition

new lemmas

new lemmas

probable fix suggested by Cornelius for the changes in the vicinity of…

discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog…

following recent Phabricator update, after 2021 Week 13 (Late March);

Fixes due to new order prover

merged

Cosmetic: no !! in the lemma statement

clarified README;

more standard header, with utf-8 encoding;

clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;

another broken proof

Fixed and simplified some failing proofs

merged

new automatic order prover: stateless, complete, verified

clarified signature;

clarified: follow "isabelle version -t";

further clarification of Isabelle distribution identification -- avoid odd…

more robust and uniform ISABELLE_TAGS;

tuned signature -- more explicit types;

simplified release status (again), in contrast to a43898f76ae9;

clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;

more uniform HTTP resources;

clarified (again): local tip could be actually more recent;

tuned;

tuned;

clarified name;

more systematic java_library: avoid empty entries, declaration order as for…

Writing less_sets as an infix

support sequential LaTeX jobs: more robust when TeX installation is self…

avoid symblinks --- make it work on Windows;

Fixed some looping proofs (though why they were looping isn't clear)

updated to latest latex due to new mechanism for dealing with bold ccfonts

Fixed a failing proof

fixes for new hd_rev and last_rev

merged

removal of needless hypothesis in hd_rev and last_rev

merge from afp-2021

merged

Infix notation for the less_sets relation

simplified a few proofs

sitegen and metadata for Constructive_Cryptography_CM

new entry Constructive_Cryptography_CM

more robust;

clarified message;

tuned;

proper export;

tuned message;

more options: build is part of default setup;

misc tuning and clarification;

more options;

proper Admin script, outside the settings environment;

tuned whitespace;

tuned;

clarified;

tuned message;

tuned message;

more accurate settings after update of current version;

clarified messages;

more robust: lest hg work out remote tip;

more options;

clarified treatment of multiple versions: last one counts;

more robust;

more robust: explicit repository root;

more robust;

more convenient repository setup;

more robust invocation of hg;

tuned;