Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. added Height_Balanced_Trees
  2. documentation of relevant ideas
  3. numeral rules for take_bit / drop_bit on int
  4. opaque export does not work as expected in presence of dependent instances
Changeset 71801:49d8d8ad7e43 by nipkow:
added Height_Balanced_Trees
The file was addedsrc/HOL/Data_Structures/Height_Balanced_Tree.thy
The file was modified src/HOL/Data_Structures/AVL_Set.thy (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 71800:35a951ed2e82 by haftmann:
documentation of relevant ideas
The file was modified src/HOL/ex/Bit_Operations.thy (diff)
Changeset 71799:e00712b4e2c2 by haftmann:
numeral rules for take_bit / drop_bit on int
The file was modified src/HOL/Parity.thy (diff)
Changeset 71798:fc4f9dad5292 by haftmann:
opaque export does not work as expected in presence of dependent instances
The file was modified src/Tools/Code/code_ml.ML (diff)