added command hg_setup: setup remote vs. local Mercurial repository;

clarified signature;

clarified signature;

tuned;

clarified signature; tuned;

tuned;

more repository information;

more permissive string fields;

tuned proof (by Thomas Sewell)

tuned;

clarified signature: error_code may contain low-level message instead of proper "ERR-" code;

clarified signature; more operations;

tuned signature;

support for conduit API;

tuned whitespace;

more robust: support /usr/local/bin/hg;

tuned documentation;

eliminated pointless option -T: it merely tests ssh config of root, which is not required later;

slicker proofs (used in CPP paper)

tuned NEWS;

more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;

tuned;

tuned documentation;

more checks for release;

more packages: required for svn;

more robust setup: avoid blind shot at "the latest" version;

more documentation;

proper default;

more robust: avoid accidental use of stdin;

support for Phabricator upgrade;

tuned signature;

tuned message;

avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";

more documentation;

more documentation;

proper support for multiple installations;

clarified "isabelle phabricator -l": avoid surprise with non-existent default installation;

tuned index.html;

more robust;

more robust;

clarified website: redirect to isabelle-dev Phabricator Overview;

more documentation;

tuned;

support database dump;

proper check of Linux version;

tuned;

proper mysql user setup: avoid superuser powers in production; specific phabricator.cache-namespace, following standard cluster configuration by Phacility;

support for pwgen;

NEWS, CONTRIBUTORS, and documentation

an extensive example for lift_bnf across quotients

extension of lift_bnf to support quotient types

unfold intermediate (internal) pred definitions

corrected some confusing terminology / notation

Ramsey with multiple colours and arbitrary exponents

a few new and tidier proofs (mostly about finite sets)

clarified signature: store full theory name;

merged

moved lemmas

merged

suppress record types: not working properly;

removed junk;

discontinued somewhat pointless options;

tuned signature;

clarified signature;

export datatypes;

clarified modules;

misc tuning and clarification: proper check of datatype kind;

clarified modules;

cleaning

tuned

separated Affine theory from Convex

merged

tuned

proper table data structure

removed some vain declarations

merged

made Starlike independent of Abstract_Limits

more direct accessors for simpset

regular merge with no historization, in accordance with regular update

moved starlike where it belongs

merged

clarified messages streaming (again, amending 5ea3ed3c52b3): avoid too many small messages stacking up, e.g. when loading HOL-Analysis.Analysis.thy into Isabelle/jEdit;

moved segment lemmas where they belong

merged

moved lemmas

merged

two new theorems

moved lemma

made internal name generation in case expressions more robust

merged

clarified export of consts: recursion is accessible via spec_rules;

more operations;

Removed orphaned theory from HOL-Analysis

merged

clarified position for spec rule: like entity;

clarified name: avoid clashes;

proper dynamic position of application context, e.g. relevant for 'global_interpretation';

proper treatment of variable names;

proper spec_rule name via naming/binding/Morphism.binding;

more informative spec rules;

more robust;

more informative export;

tuned signature -- following Export_Theory.Spec_Rule in Scala;

tuned comment;

clarified export of spec rules: more like locale;

formal position for spec rule (not significant for equality);

proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory";

proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory";

tuned -- avoid confusion of fun_t with fun_lhs;

avoid shadowing of local bindings -- more maintainable;

export spec rules;

Reorganised HOL-Complex_Analysis

split off metric spaces part of Function_Topology: subsequent theories Product_Topology, T1_Spaces, Lindelof_Spaces are purely topological

merged

tuned Analysis manual

tuned Analysis manual

more rules

tuned material

tuned manual

Removed duplicate theorems from HOL-Analysis

Flattened dependency tree of HOL-Analysis

Merged

Simplified Harmonic_Numbers

Split off new HOL-Complex_Analysis session from HOL-Analysis

merged

tuned Analysis/Analysis;

characterization of typical bit operations

merged

renamed Analysis/Winding_Numbers to Winding_Numbers_2; reorganised Analysis/Cauchy_Integral_Theorem by splitting it into Contour_Integration, Winding_Numbers,Cauchy_Integral_Theorem and Cauchy_Integral_Formula.

transfer rule for bit operation

characterization of singleton bit operation

bit accessor and fundamental properties

merged

more informative spec rules: optional name; clarified signature; more thorough treatment of Thm.trim_context vs. Thm.transfer;

proper theory context, e.g. for Thm.transfer;

more structural integrity;

tuned

reduced imports; deleted unusewd minor lemmas for that purpose

tuned

reduced imports and removed unused material

tuned

merged

reduced imports

Fixed a few messy proofs and adjusted inconsistent section headings

A more informative comment

Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.

Remove diagnostic command 'print_dependencies'.

support for output messages;

tuned;

tuned -- avoid deprecated constructors;

tuned signature;

avoid vacuous session Pure -- dump does not read_pure_theory;

updated to polyml-5.8.1-20191113 test version (Poly/ML 055f20cdc326);

clarified vacuous selection vs. Pure;

tuned signature;

tuned theory structure

more robust: size varies due to different position information in "isabelle build" vs. "isabelle dump";

clarified signature;

tuned proofs;

clarified error: tmp file can be invalid in odd situations;

more robust: file length can be invalid in odd situations;

tuned;

tuned whitespace

proper prefix syntax

removed unused auxiliary lemmas

tuned;

added document antiquotation @{system_option};

improved performance of session exports via bulk transactions;

tuned signature;

support for bulk operations: consume mailbox content in batches;

clarified signature -- more explicit types;

tuned signature -- more operations;

tuned

tuned

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;

more robust expose_proofs corresponding to register_proofs/consolidate_theory; expose_proofs of class algebra more aggresively, to ensure early export within original theory/session context;

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

clarified errors;

determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);

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

oops — fixed symbols!!

reorganisation to eliminate Brouwer_Fixpoint from complex analysis

merged

Inverse function theorem + lemmas

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

unused;

unused;

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

clarified signature;

tuned;

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

more scalable protocol_message: use XML.body directly (Output.output hook is not required);

clarified signature;

tuned;

updated to polyml-5.8.1-20191101 test version;

merged

more operations;

proper export of unnamed proof boxes for unnamed toplevel declarations, e.g. rulify/defn rules in theory IFOL and HOL;

clarified signature (again);

clarified signature;

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

avoid redundant proof boxes for application sessions;

clarified modules (again);

more detailed proof term output; tuned signature;

tuned signature;

clarified error;

more accurate proof_boxes -- from actual proof body;

clarified signature;

clarified signature;

more lemmas

merged

linear is not needed

more packages;

MySQL setup; tuned;

Apache setup; proper "-" for URL: avoid problems with "_";

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;

Removed dup lemma that inhibited locale instantiations (dup fact error)

some applications of "metric"

header with Title/Author; added note on motivation of this example

a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler

NEWS

added examples for "metric" method, by Maximilian Schäffeler

added contributor

avoid referring to lemmas by index

documented reference

example applications of the 'metric' decision procedure, by Maximilian Schäffeler

decision procedure for metric spaces, implemented by Maximilian Schäffeler

NEWS

renamed because of duplicateion to avoid very long qualified names

proper order of variables, independently of varify/unvarify state -- relevant for export of locale conclusions;

merged

clarified session_graph_display: restrict sessions to actually required theories;

removed dummy ATP

compile

tuning

invoke remote Vampire with higher-order (THF) syntax

repaired remote_vampire's proof reconstruction

added support for Zipperposition on SystemOnTPTP

folded experimental Ehoh into E now that E 2.3 has been released

removed support for old system E-MaLeS

added support for repote Alt-Ergo

updated nomenclature for TPTP languages to use modern three-symbol abbreviations (e.g. TF1)

removed support for E-ToFoF, which has lost its raison d'etre since E 2.0 supports TF0

removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)

removed support for iProver-Eq

updated iProver setup and tuned other ATP setups

removed experimental encoding for Waldmeister

removed support for remote Satallax because its output does not clearly identify the lemmas used

changed Satallax's setup to invoke E