David Matthews <dm@prolingua.co.uk> committed rPOLYMLa01fead649bc: Fix reading remote statistics in Unix. (authored by David Matthews <dm@prolingua.co.uk>).

David Matthews <dm@prolingua.co.uk> committed rPOLYML67e87c763417: Run a major GC is the cumulative cost of the minor GCs since the last major GC… (authored by David Matthews <dm@prolingua.co.uk>).

haftmann committed rISABELLEa197532693a5: bit shifts as class operations.

haftmann committed rISABELLEb7d481cdd54d: new lemma.

Lars Hupel <lars.hupel@mytum.de> committed rAFPf1ef07c47429: don't build Linear_Programming on Mac.

wenzelm committed rISABELLE3c04a52c422a: tuned comments;.

wenzelm committed rISABELLEfd82d53c1761: merged.

wenzelm committed rISABELLE06c6495fb1d0: retain type information from reconstruct_proof, notably for Export_Theory..

wenzelm committed rISABELLE4b45d592ce29: clarified modules;.

wenzelm committed rISABELLE907b7a6471a0: tuned proofs;.

wenzelm committed rISABELLE77580c977e0c: more robust;.

wenzelm committed rISABELLEaedd11603fb4: tuned modules;.

wenzelm committed rISABELLE950e1cfe0fe4: tuned proofs -- more stable proof terms without [rule_format];.

paulson committed rISABELLEc4458eb355c0: merged.

paulson <lp15@cam.ac.uk> committed rISABELLEce92360f0692: A slight tidying up of messy proof steps.

wenzelm committed rISABELLE995fe5877d53: tuned declarations for more compact proof terms;.

wenzelm committed rISABELLE45a1fcee14a0: prefer named facts;.

wenzelm committed rISABELLE64249a83bc29: clarified contexts;.

wenzelm committed rISABELLEe06852132c1d: tuned messages;.

wenzelm committed rISABELLE5bb2235d843d: clarified command-line;.

wenzelm committed rISABELLE41b6ca223500: tuned messages;.

wenzelm committed rISABELLE8ac137c65776: tuned messages;.

wenzelm committed rISABELLE70205e023cb4: more messages -- expose potential database problems;.

wenzelm committed rISABELLE324c40205fc8: clarified errors: include stdout;.

wenzelm committed rISABELLEd61fd7aade69: clarified directory;.

wenzelm committed rISABELLE22fcdadc404d: tuned;.

wenzelm committed rISABELLE9ce299019d21: tuned message;.

wenzelm committed rISABELLE79b89278b825: clarified permissions;.

wenzelm committed rISABELLE9314a4cc84ea: merged.

wenzelm committed rISABELLE510b89906d86: discontinued somewhat pointless Isabelle options: setup implicitly assumes….

wenzelm committed rISABELLE67cbf2e52785: unused;.

wenzelm committed rISABELLE114db2b5a5f8: support for Phabricator mail configuration;.

traytel committed rISABELLE98ac9a4323a2: merged.

traytel committed rISABELLEc9c1a64eeb69: corrected typo in lemma name.

nipkow committed rISABELLEd628bbdce79a: moved lemma.

traytel committed rISABELLEb3956a37c994: merged.

traytel committed rISABELLE1d19e844fa4d: characterization of until in terms of strong until (and vice versa)….

nipkow committed rISABELLE295609359b58: tuned toc.

nipkow committed rAFP54f6a4f1d8a3: updated to fdb6c5034c24.

immler committed rAFP2a06a089800f: merged.

paulson <lp15@cam.ac.uk> committed rAFP3f2bdb753c38: patched a proof.

immler committed rAFPc5944c920143: moved Interval and Interval_Approximation to isabelle.

wenzelm committed rISABELLE9b531e611d66: merged.

wenzelm committed rISABELLE2965304143d8: more phabricator setup;.

wenzelm committed rISABELLE6ca9e8377613: proper names for multiple installations;.

wenzelm committed rISABELLEee3c43eb79ae: proper service name (again): it is specific to each installation;.

wenzelm committed rISABELLEb64fc38327ae: prefer system user setup, e.g. avoid occurrence on login screen;.

wenzelm committed rISABELLE27a998cdc0f4: back to plain name, to have it accepted my mysql;.

wenzelm committed rISABELLEba14aa0b5a5d: more robust: install PHP daemon after Apache;.

wenzelm committed rISABELLE6bf53035baf0: clarified name prefixes: global config always uses "isabelle-phabricator";.

wenzelm committed rISABELLE8198ceef0301: more phabricator setup;.

wenzelm committed rISABELLE4eeff87c5072: more phabricator setup;.

wenzelm committed rISABELLEf4b9dd5ab0cc: more phabricator setup;.

wenzelm committed rISABELLE5f02ecbb19d6: support for system services;.

wenzelm committed rISABELLE87c132cf5860: more options;.

wenzelm committed rISABELLEb8aeeedf7e68: support for Linux user management;.

nipkow committed rISABELLE9858f391ed2d: merged.

nipkow committed rISABELLEcb504351d058: tuned.

nipkow committed rISABELLE2fab72ab919a: moved duplicate lemmas up the hierarchy.

haftmann committed rISABELLE400e9512f1d3: proof-of-concept theory for bit operations without a constructivistic….

nipkow committed rISABELLEfdb6c5034c24: merged.

nipkow committed rISABELLE9d2753406c60: removed redundant lemma.

immler committed rISABELLEddd4aefc540f: merged.

immler committed rISABELLEbd3d4702b4f2: add lemmas.

immler committed rISABELLEf630f2e707a6: refactor Approximation.thy to use more abstract type of intervals.

immler committed rISABELLEdfcc1882d05a: moved theory Interval_Approximation from the AFP.

immler committed rISABELLE6fe5a0e1fa8e: moved theory Interval from the AFP.

immler committed rISABELLEe0755162093f: replace approximation oracle by less ad-hoc @{computation}s.

nipkow committed rISABELLEc1b63124245c: tuned.

nipkow committed rISABELLEacedd04c1a42: merged.

nipkow committed rISABELLE66c025383422: tuned.

paulson <lp15@cam.ac.uk> committed rISABELLEb6e69c71a9f6: Merge and get rid of closed_segmentI.

paulson <lp15@cam.ac.uk> committed rISABELLE934e0044e94b: Moved or deleted some out of place material, also eliminating obsolete naming….

immler committed rISABELLEc2465b429e6e: Line_Segment is independent of Convex_Euclidean_Space.

immler committed rISABELLEb212ee44f87c: the division between Starlike and Convex_Euclidean_Space is artificial….

immler committed rISABELLE12cbcd00b651: betweenness is a property on line segments.

immler committed rISABELLEbe8cec1abcbb: reduce dependencies of Ordered_Euclidean_Space; move more general material from….

wenzelm committed rISABELLE35a8e15b7e03: more robust Thm.expose_theory -- ensure that PIDE export happens in the proper….

wenzelm committed rISABELLE38bed2483e6a: proper message (amending 94442fce40a5);.

wenzelm committed rISABELLEb697dd74221a: tuned;.

wenzelm committed rISABELLE6504ea98623c: uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with….

wenzelm committed rISABELLE4003da7e6a79: updated xml_size;.

wenzelm committed rISABELLEc9f5f724abc0: prefer named result;.

wenzelm committed rISABELLEd32ed8927a42: more robust expose_proofs corresponding to register_proofs/consolidate_theory;.

wenzelm committed rISABELLEc85efa2be619: expose derivations more thoroughly, notably for locale/class reasoning;.

wenzelm committed rISABELLEbb49abc2ecbb: determine proof boxes from exported proof (NB: thm_boxes is not sufficient due….

wenzelm committed rISABELLEb05d78bfc67c: clarified errors;.

wenzelm committed rISABELLE58022ee70b35: more operations;.

wenzelm committed rISABELLEbfa1017b4553: tuned whitespace;.

wenzelm committed rISABELLE73f14e0b7151: more robust;.

wenzelm committed rISABELLE2c96e48027eb: clarified modules;.

wenzelm committed rISABELLEbe689b7d81fd: clarified signature -- more options;.

paulson committed rISABELLEbb403cb94db2: merged.

paulson <lp15@cam.ac.uk> committed rISABELLEe892f7a1fd83: moved line segments to Convex_Euclidean_Space.

wenzelm committed rISABELLE15129c2f4a33: proper theory for export_proofs;.

wenzelm committed rISABELLE41685289b8eb: tuned signature;.

paulson committed rISABELLE7f1241a2bf30: merged.

paulson <lp15@cam.ac.uk> committed rISABELLEb86d30707837: just tidied one proof.

wenzelm committed rISABELLE699ff83813c0: proper graph traversal -- avoid exponential blowup (amending 71d1971d67ad);.

paulson <lp15@cam.ac.uk> committed rAFPc5c88012f116: fixed a failing (and ugly) proof.