Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. type class reduction
  3. merged
  4. de-applying and tidying
  5. early and more complete setup of tools
  6. factored out theory Bits_Int
  7. factored out singular operation into separate theory
Changeset 72493:fa4bb287ea56 by paulson:
merged
Changeset 72492:2dd41a8893aa by paulson _lp15@cam.ac.uk_:
type class reduction
The file was modified src/HOL/Analysis/Affine.thy (diff)
Changeset 72491:18e760349b86 by paulson:
merged
Changeset 72490:df988eac234e by paulson _lp15@cam.ac.uk_:
de-applying and tidying
The file was modified src/HOL/Analysis/Retracts.thy (diff)
Changeset 72489:a1366ce41368 by haftmann:
early and more complete setup of tools
The file was modified src/HOL/Word/Tools/smt_word.ML (diff)
The file was modified src/HOL/Word/Word.thy (diff)
Changeset 72488:ee659bca8955 by haftmann:
factored out theory Bits_Int
The file was modified src/HOL/Library/Bit_Operations.thy (diff)
The file was modified src/HOL/SPARK/Manual/Reference.thy (diff)
The file was modified src/HOL/SPARK/SPARK.thy (diff)
The file was modified src/HOL/Word/Bit_Comprehension.thy (diff)
The file was modified src/HOL/Word/Bits_Int.thy (diff)
The file was modified src/HOL/Word/Misc_Typedef.thy (diff)
The file was modified src/HOL/Word/Reversed_Bit_Lists.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
Changeset 72487:ab32922f139b by haftmann:
factored out singular operation into separate theory
The file was addedsrc/HOL/Word/Word_rsplit.thy
The file was modified src/HOL/Word/Bits_Int.thy (diff)
The file was modified src/HOL/Word/More_Word.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)