Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. contributors
  2. hide the internal abbreviations MR and MB
  3. optimize RBT_Impl
Changeset 73213:bb35f7f60d6c by andreas lochbihler _mail@andreas-lochbihler.de_:
contributors
The file was modified CONTRIBUTORS (diff)
Changeset 73212:87e3c180044a by andreas lochbihler _mail@andreas-lochbihler.de_:
hide the internal abbreviations MR and MB
The file was modified src/HOL/Library/RBT_Impl.thy (diff)
Changeset 73211:bfa9f646f5ae by mraszyk:
optimize RBT_Impl
The file was modified src/HOL/Library/RBT_Impl.thy (diff)