Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. lemmas about sets and the enumerate operator
  3. yet another little lemma
  4. merged
  5. merged
  6. merged
  7. strengthened a lemma
  8. A new lemma about abstract Sum / Prod
  9. separation of reversed bit lists from other material
  10. merged
  11. avoid exhaustion of worker threads, notably due to complex interaction of future/promise/lazy in Proofterm.make_thm_node;
  12. more robust: insist in finished future;
  13. unused;
  14. further refinement of code equations for mask operation
Changeset 72096:6b5421bd0fc3 by paulson:
merged
Changeset 72095:cfb6c22a5636 by paulson _lp15@cam.ac.uk_:
lemmas about sets and the enumerate operator
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Library/Infinite_Set.thy (diff)
The file was modified src/HOL/List.thy (diff)
Changeset 72094:beccb2a0410f by paulson _lp15@cam.ac.uk_:
yet another little lemma
The file was modified src/HOL/Groups_Big.thy (diff)
Changeset 72093:6a2f43901350 by paulson:
merged
Changeset 72092:3f8e6c0166ac by paulson:
merged
Changeset 72091:b6065cbbf5e2 by paulson:
merged
Changeset 72090:5d17e7a0825a by paulson _lp15@cam.ac.uk_:
strengthened a lemma
The file was modified src/HOL/Library/Infinite_Set.thy (diff)
Changeset 72089:8348bba699e6 by paulson _lp15@cam.ac.uk_:
A new lemma about abstract Sum / Prod
The file was modified src/HOL/Groups_Big.thy (diff)
Changeset 72088:a36db1c8238e by haftmann:
separation of reversed bit lists from other material
The file was addedsrc/HOL/Word/Reversed_Bit_Lists.thy
The file was modified NEWS (diff)
The file was modified src/HOL/Word/Bits_Int.thy (diff)
The file was modified src/HOL/Word/Misc_lsb.thy (diff)
The file was modified src/HOL/Word/Misc_msb.thy (diff)
The file was modified src/HOL/Word/More_Word.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was removedsrc/HOL/Word/Bit_Lists.thy
Changeset 72087:43a43b182a81 by wenzelm:
merged
Changeset 72086:41e1e2395a67 by wenzelm:
avoid exhaustion of worker threads, notably due to complex interaction of future/promise/lazy in Proofterm.make_thm_node;
The file was modified src/Pure/Concurrent/future.ML (diff)
Changeset 72085:3afd6b1c7ab5 by wenzelm:
more robust: insist in finished future;
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Concurrent/lazy.ML (diff)
Changeset 72084:df99d26efeeb by wenzelm:
unused;
The file was modified src/Pure/Concurrent/future.ML (diff)
Changeset 72083:3ec876181527 by haftmann:
further refinement of code equations for mask operation
The file was modified src/HOL/Library/Bit_Operations.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)