Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. hide spurious defining equation; tuned
  2. merged
  3. merged
  4. merged
  5. proper code adaptation for Eval target to avoid refinement of underspecification
Changeset 8423:04602c3b71e9 by Andreas Lochbihler:
hide spurious defining equation; tuned
The file was modified thys/Native_Word/Native_Word_Test.thy (diff)
The file was modified thys/Native_Word/Uint.thy (diff)
Changeset 8422:260f94d27f45 by Andreas Lochbihler:
merged
Changeset 8421:d99aae0ec655 by Andreas Lochbihler:
merged
Changeset 8420:ff121cd97ba2 by Andreas Lochbihler:
merged
Changeset 8419:78e6093fd54d by Andreas Lochbihler:
proper code adaptation for Eval target to avoid refinement of underspecification
The file was modified thys/Native_Word/Uint32.thy (diff)
The file was modified thys/Native_Word/Uint64.thy (diff)
The file was modified thys/Native_Word/Uint8.thy (diff)