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

more transfer rules

tuned syntax

bit operations form an boolean algebra

bit operations for word type

no printing of axioms -- too bulky;

clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;

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

clarified types (again): 'a is canonical for 'class' (as alternative to 'locale'), 'b is common for Hindley-Milner examples;

export constdefs according to defs.ML;

avoid spurious shyps (with vacous type variable);

merged

more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;

clarified signature: name of standard_proof is authentic, otherwise empty;

clarified expand_proof/expand_name: allow more detailed control via thm_header; export_standard_proofs: authentic theorem names in "print" format;

option to export standardized proof terms (not scalable);

more kinds, notably for Isabelle/MMT;

refined proof of concept for bit operations

more lemmas

merged

export toplevel proof similar to named PThm;

tuned signature;

proper protocol_message for bootstrap proofs;

proper export of bootstrap proofs (amending a6304b4664b6);