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];

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

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;

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;

proper theory for export_proofs;

tuned signature;

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

back to more elementary Buffer.T -- less intermediate garbage;

unused;

unused;

clarified signature;

more direct output of XML material -- bypass Buffer.T;

tuned;

more direct output of XML material -- bypass Buffer.T;

more scalable protocol_message: use XML.body directly (Output.output hook is…

clarified signature;

tuned;

updated to polyml-5.8.1-20191101 test version;

merged

clarified signature (again);

proper export of unnamed proof boxes for unnamed toplevel declarations, e.g.

more operations;

clarified signature;

avoid redundant proof boxes for application sessions;

make double-sure that internal proof boxes are exported, e.g. in Pure;

clarified modules (again);

more detailed proof term output;

clarified error;

tuned signature;

more accurate proof_boxes -- from actual proof body;

clarified signature;

clarified signature;

more packages;

MySQL setup;

Apache setup;

some support for Phabricator server;

support for Linux packages;

specific support for Linux, notably Ubuntu/Debian;

proper home directory, required for $HOME/.ssh setup;

merged

proper file name: .ML is mandatory for Isabelle/ML files;

proper order of variables, independently of varify/unvarify state -- relevant…

merged

clarified session_graph_display: restrict sessions to actually required…

no printing of axioms -- too bulky;

clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for…

more conservative type names, e.g. relevant for Isabelle/MMT export;

clarified types (again): 'a is canonical for 'class' (as alternative to…

export constdefs according to defs.ML;