Summary
- merged
- merged
- simplified proofs
- some information about Phabricator server setup;
- More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.
The file was modified | src/HOL/Data_Structures/Balance.thy (diff) |
The file was added | Admin/Phabricator/README |
The file was added | Admin/Phabricator/ssh/ssh-hook |
The file was added | Admin/Phabricator/ssh/sshd-phabricator.service |
The file was added | Admin/Phabricator/ssh/sshd_config.phabricator |
The file was added | Admin/Phabricator/ssh/sudoers.d/phabricator |
The file was added | Admin/Phabricator/update |
The file was modified | src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy (diff) |
The file was modified | src/HOL/Orderings.thy (diff) |
The file was modified | src/HOL/Set_Interval.thy (diff) |
The file was modified | src/HOL/Tools/SMT/smt_replay.ML (diff) |
The file was modified | src/HOL/Topological_Spaces.thy (diff) |
The file was modified | src/HOL/Transitive_Closure.thy (diff) |
The file was modified | src/HOL/Word/Word.thy (diff) |