strengthened type class for bit operations

tuned

tuned

more packages;

NEWS;

more examples;

more documentation;

misc tuning and clarification;

merged

tuned PHP setup;

clarified errors: PHP daemon can fail under odd circumstances;

more robust;

tuned message;

more sanity checks;

just one isabelle-phabricator-phd service, which manages all processes uniformly (NB: "bin/phd stop" affects all installations);

clarified signature: allow compound arg;

clarified signature;

merged

tuned tags

more portable;

updated to polyml-5.8.1-20191114: rebuilt on Windows with current msys2/mingw64;

updated MinGW installation: requires Cygwin from Isabelle2018 to avoid problems with address relocation;

tuned;

tuned;

clarified signature;

updated to polyml-5.8.1-20191113 test version (Poly/ML 67e87c763417);

more support for multiple daemons;

more robust: system ssh service is required for Phabricator ssh service;

removed obsolete material: already covered by documentation or tools;

configure SSH hosting via "isabelle phabricator_setup_ssh"; tuned message;

more robust;

clarified signature; more operations;

removed obsolete material -- already covered by "system" manual; tuned;

tuned;

merged

more documentation; tuned;

tuned;

more options;

clarified Console_Progress.echo: include empty lines as in other Progress instances, especially relevant for Progress.bash (e.g. "isabelle phabricator ./bin/config help");

documentation on Phabricator server administration;

tuned message;

added "isabelle phabricator";

New library material from the AFP entry ZFC_in_HOL

tuned order between theories

bit shifts as class operations

new lemma

tuned comments;

merged

retain type information from reconstruct_proof, notably for Export_Theory.export_thm;

tuned proofs;

clarified modules;

more robust;

tuned modules;

tuned proofs -- more stable proof terms without [rule_format];

merged

A slight tidying up of messy proof steps

tuned declarations for more compact proof terms;

prefer named facts; tuned signature;

clarified contexts; prefer named facts;

tuned messages;

clarified command-line;

tuned messages;

tuned messages;

more messages -- expose potential database problems;

clarified errors: include stdout;

clarified directory;

tuned;

tuned message;

clarified permissions;

merged

discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;

unused;

support for Phabricator mail configuration; discontinued template for "isabelle phabricator_update" -- is likely to become a plain shell script;

merged

corrected typo in lemma name

moved lemma

merged

characterization of until in terms of strong until (and vice versa), contributed by Michael Foster

tuned toc

merged

proper names for multiple installations;

more phabricator setup;

proper service name (again): it is specific to each installation;

back to plain name, to have it accepted my mysql;

prefer system user setup, e.g. avoid occurrence on login screen;

more robust: install PHP daemon after Apache;

clarified name prefixes: global config always uses "isabelle-phabricator";

more phabricator setup;

more phabricator setup;

more phabricator setup;

support for system services;

more options;

support for Linux user management;

merged

tuned

moved duplicate lemmas up the hierarchy

proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation

merged

removed redundant lemma

merged

add lemmas

refactor Approximation.thy to use more abstract type of intervals

moved theory Interval_Approximation from the AFP

moved theory Interval from the AFP

replace approximation oracle by less ad-hoc @{computation}s

tuned

merged

tuned

Merge and get rid of closed_segmentI

Moved or deleted some out of place material, also eliminating obsolete naming conventions

Line_Segment is independent of Convex_Euclidean_Space

the division between Starlike and Convex_Euclidean_Space is artificial, therefore include Starlike

betweenness is a property on line segments

reduce dependencies of Ordered_Euclidean_Space; move more general material from Cartesian_Euclidean_Space

proper message (amending 94442fce40a5);

more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;

uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of re-used nodes;

tuned;

updated xml_size;

prefer named result;