Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more elementary rules about div / mod on int
  2. complete set of cases rules for integers known to be (non-)positive/negative; legacy theorem branding
  3. more facts on sgn, abs
  4. dropped slightly outdated comment
Changeset 64715:33d5fa0ce6e5 by haftmann:
more elementary rules about div / mod on int
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Power.thy (diff)
Changeset 64714:53bab28983f1 by haftmann:
complete set of cases rules for integers known to be (non-)positive/negative;<br>legacy theorem branding
The file was modified src/HOL/Int.thy (diff)
Changeset 64713:9638c07283bc by haftmann:
more facts on sgn, abs
The file was modified src/HOL/Rings.thy (diff)
Changeset 64712:38adf0c59c35 by haftmann:
dropped slightly outdated comment
The file was modified src/HOL/Nat.thy (diff)