Skip to content
Success

Changes

Summary

  1. merged
  2. merged
  3. simplified proofs
  4. some information about Phabricator server setup;
  5. More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.
Changeset 70753:c5232e6fb10b by nipkow:
merged
Changeset 70752:401cd34711b5 by nipkow:
merged
Changeset 70751:fd9614c98dd6 by nipkow:
simplified proofs
The file was modified src/HOL/Data_Structures/Balance.thy (diff)
Changeset 70750:07673e7cb5e6 by wenzelm:
some information about Phabricator server setup;
The file was addedAdmin/Phabricator/README
The file was addedAdmin/Phabricator/ssh/ssh-hook
The file was addedAdmin/Phabricator/ssh/sshd-phabricator.service
The file was addedAdmin/Phabricator/ssh/sshd_config.phabricator
The file was addedAdmin/Phabricator/ssh/sudoers.d/phabricator
The file was addedAdmin/Phabricator/update
Changeset 70749:5d06b7bb9d22 by paulson _lp15@cam.ac.uk_:
More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.
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)