New library material from the AFP entry ZFC_in_HOL

tuned order between theories

bit shifts as class operations

new lemma

don't build Linear_Programming on Mac

tuned comments;

merged

retain type information from reconstruct_proof, notably for Export_Theory.

clarified modules;

tuned proofs;

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;

clarified contexts;

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…

unused;

support for Phabricator mail configuration;

merged

corrected typo in lemma name

moved lemma

merged

characterization of until in terms of strong until (and vice versa)…

tuned toc

updated to fdb6c5034c24

merged

patched a proof

moved Interval and Interval_Approximation to isabelle

merged

more phabricator setup;

proper names for multiple installations;

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

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

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

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…

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…

Line_Segment is independent of Convex_Euclidean_Space

the division between Starlike and Convex_Euclidean_Space is artificial…

betweenness is a property on line segments

reduce dependencies of Ordered_Euclidean_Space; move more general material from…

more robust Thm.expose_theory -- ensure that PIDE export happens in the proper…

proper message (amending 94442fce40a5);

tuned;

uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with…

updated xml_size;

prefer named result;

more robust expose_proofs corresponding to register_proofs/consolidate_theory;

expose derivations more thoroughly, notably for locale/class reasoning;

determine proof boxes from exported proof (NB: thm_boxes is not sufficient due…

clarified errors;

more operations;

tuned whitespace;

more robust;

clarified modules;

clarified signature -- more options;

merged

moved line segments to Convex_Euclidean_Space

proper theory for export_proofs;

tuned signature;

merged

just tidied one proof

proper graph traversal -- avoid exponential blowup (amending 71d1971d67ad);

fixed a failing (and ugly) proof