Summary
- 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