paulson <lp15@cam.ac.uk> committed rISABELLE9d0712c74834: oops — fixed symbols!!.

paulson <lp15@cam.ac.uk> committed rISABELLE3e374c65f96b: reorganisation to eliminate Brouwer_Fixpoint from complex analysis.

paulson committed rISABELLE98308c6582ed: merged.

paulson <lp15@cam.ac.uk> committed rISABELLE5b753486c075: Inverse function theorem + lemmas.

wenzelm committed rISABELLE7926d2fc3c4c: back to more elementary Buffer.T -- less intermediate garbage;.

wenzelm committed rISABELLE325247f32da9: unused;.

wenzelm committed rISABELLEebdfd6c43e56: unused;.

wenzelm committed rISABELLEff11af12dfdd: clarified signature;.

wenzelm committed rISABELLE2c17fa0f5187: more direct output of XML material -- bypass Buffer.T;.

wenzelm committed rISABELLE2e610951f79a: tuned;.

wenzelm committed rISABELLEe7dfc505de1b: more direct output of XML material -- bypass Buffer.T;.

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

wenzelm committed rISABELLEe5e34bd28257: clarified signature;.

wenzelm committed rISABELLE64a20b562e63: tuned;.

wenzelm committed rISABELLE38ade730f6df: updated to polyml-5.8.1-20191101 test version;.

wenzelm committed rISABELLE6178ecf357a0: merged.

wenzelm committed rISABELLE5e98925f86ed: clarified signature (again);.

wenzelm committed rISABELLE2866fee241ee: proper export of unnamed proof boxes for unnamed toplevel declarations, e.g..

wenzelm committed rISABELLEd8a7df9fdd03: more operations;.

wenzelm committed rISABELLE52a62342c9ce: clarified signature;.

wenzelm committed rISABELLEa802d42c00bc: avoid redundant proof boxes for application sessions;.

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

wenzelm committed rISABELLE9dab828cbbc1: clarified modules (again);.

wenzelm committed rISABELLE7abe5abb4c05: more detailed proof term output;.

wenzelm committed rISABELLE397533bf0c3f: clarified error;.

wenzelm committed rISABELLEa1c137961c12: tuned signature;.

wenzelm committed rISABELLEd86798eddc14: more accurate proof_boxes -- from actual proof body;.

wenzelm committed rISABELLE19818f99b4ae: clarified signature;.

wenzelm committed rISABELLE3ee90f831805: clarified signature;.

haftmann committed rISABELLEa7a52ba0717d: more lemmas.

Andreas Halkjær From <s144442@student.dtu.dk> committed rAFP1f17a5f5a1e2: Merge branch.

Andreas Halkjær From <s144442@student.dtu.dk> committed rAFPf05300d8017a: Tuned spacing..

immler committed rISABELLE196b41b9b9c8: merged.

immler committed rISABELLE82057e7b9ea0: linear is not needed.

wenzelm committed rISABELLE80dfc9a2f9c8: more packages;.

wenzelm committed rISABELLEa48112873f81: MySQL setup;.

wenzelm committed rISABELLE46847076477c: Apache setup;.

wenzelm committed rISABELLE79736ffe77c3: some support for Phabricator server;.

wenzelm committed rISABELLEacc3bac0d7c5: support for Linux packages;.

wenzelm committed rISABELLEfe9496df6298: specific support for Linux, notably Ubuntu/Debian;.

David Matthews <dm@prolingua.co.uk> committed rPOLYML51f3ce2ae95f: Change some instances of POLYUNSIGNED to uintptr_t. The values can overflow 32… (authored by David Matthews <dm@prolingua.co.uk>).

makarius added a member for isabelle-repository: immler.

immler updated immler.

wenzelm committed rISABELLE99eec58dc551: proper home directory, required for $HOME/.ssh setup;.

wenzelm committed rISABELLEbbe5fe8bba71: merged.

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

Peter Lammich committed rISABELLE70fb697be418: Removed dup lemma that inhibited locale instantiations (dup fact error).

immler committed rISABELLE84f79d82df0a: some applications of "metric".

immler committed rISABELLEba0b65d45aec: header with Title/Author; added note on motivation of this example.

immler committed rISABELLEe8fc52f3f175: a slower implementation of the "metric" method as Eisbach example, by….

immler committed rISABELLEaa41be39aa99: NEWS.

immler committed rISABELLE860198428664: added examples for "metric" method, by Maximilian Schäffeler.

immler committed rISABELLE73ae8c30c6cb: added contributor.

immler committed rISABELLE23e6eef4e6aa: avoid referring to lemmas by index.

immler committed rISABELLE420359ba6acd: documented reference.

immler committed rISABELLEf140135ff375: example applications of the 'metric' decision procedure, by Maximilian….

immler committed rISABELLE678b2abe9f7d: decision procedure for metric spaces, implemented by Maximilian Schäffeler.

nipkow committed rISABELLE7378fa1d0892: NEWS.

nipkow committed rAFP877fab13602e: follow devel changeset 581083959358.

nipkow committed rISABELLE581083959358: renamed because of duplicateion to avoid very long qualified names.

wenzelm committed rISABELLE5ed8c7e826a2: proper order of variables, independently of varify/unvarify state -- relevant….

wenzelm committed rISABELLEb62bb9a61abc: merged.

wenzelm committed rISABELLE79d23e6436d0: clarified session_graph_display: restrict sessions to actually required….

Andreas Halkjær From <s144442@student.dtu.dk> committed rAFP1a0be182fdda: Consistent spacing in set comprehension and name fixes..

Andreas Halkjær From <s144442@student.dtu.dk> committed rAFP616e41c5089c: Consistent spacing in set comprehension..

blanchet committed rISABELLE420f5d1953c7: removed dummy ATP.

blanchet committed rISABELLE849311b45428: compile.

blanchet committed rISABELLEccc771091a78: tuning.

blanchet committed rISABELLE718255bde391: invoke remote Vampire with higher-order (THF) syntax.

blanchet committed rISABELLEd4ef7617e31e: repaired remote_vampire's proof reconstruction.

blanchet committed rISABELLEce3a05ad07b7: added support for Zipperposition on SystemOnTPTP.

blanchet committed rISABELLE3218999b3715: folded experimental Ehoh into E now that E 2.3 has been released.

blanchet committed rISABELLE646651bcf261: updated nomenclature for TPTP languages to use modern three-symbol….

blanchet committed rISABELLE6d84c3c333d5: removed support for old system E-MaLeS.

blanchet committed rISABELLEfe114eca312e: added support for repote Alt-Ergo.

blanchet committed rISABELLE25c1ff13dbdb: removed E-SInE, a very old system by now (and SInE has been incorporated in….

blanchet committed rISABELLE535ff1eac86c: removed support for E-ToFoF, which has lost its raison d'etre since E 2.0….

blanchet committed rISABELLE600da8ccbe5b: removed support for iProver-Eq.

blanchet committed rISABELLEa35618d00d29: updated iProver setup and tuned other ATP setups.

blanchet committed rISABELLE1d2b2cc792f1: removed experimental encoding for Waldmeister.

blanchet committed rISABELLE1019b8609552: removed support for remote Satallax because its output does not clearly….

blanchet committed rISABELLE9b69bb9c1c8d: changed Satallax's setup to invoke E.

nipkow committed rAFPba01b2eda5e4: updated email.

haftmann committed rISABELLE273fc913427b: more transfer rules.

haftmann committed rISABELLEcc204e10385c: tuned syntax.

haftmann committed rISABELLEb4564de51fa7: bit operations form an boolean algebra.

haftmann committed rISABELLE525853e4ec80: bit operations for word type.

wenzelm committed rISABELLE15758fced053: no printing of axioms -- too bulky;.

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

wenzelm committed rISABELLE539dfd4c166b: more conservative type names, e.g. relevant for Isabelle/MMT export;.

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

wenzelm committed rISABELLE1e0ad25c94c8: export constdefs according to defs.ML;.

wenzelm committed rAFPc85fcabd5bff: avoid name clash of internal derivations;.

wenzelm committed rAFP9bd3fa01955a: recovered proof;.

kleing committed rAFP6a3c69467146: Clean: ROOT/directories structure.

wenzelm committed rISABELLE692095bafcd9: avoid spurious shyps (with vacous type variable);.

wenzelm committed rISABELLEd36f600c6500: merged.

wenzelm committed rISABELLE693e811b91bb: more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;.

wenzelm committed rISABELLE4c15217d6266: clarified signature: name of standard_proof is authentic, otherwise empty;.

wenzelm committed rISABELLEbd4d37edfee4: clarified expand_proof/expand_name: allow more detailed control via thm_header;.