Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. fixed the proof of pair_measure_count_space
  2. merged
  3. fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring
  4. merged
  5. type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
Changeset 67693:4fa9d5ef95bc by paulson _lp15@cam.ac.uk_:
fixed the proof of pair_measure_count_space
The file was modified src/HOL/Analysis/Binary_Product_Measure.thy (diff)
Changeset 67692:19c77698a48d by paulson:
merged
Changeset 67691:db202a00a29c by paulson _lp15@cam.ac.uk_:
fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
Changeset 67690:3c02b0522e23 by paulson:
merged
Changeset 67689:2c38ffd6ec71 by paulson _lp15@cam.ac.uk_:
type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
The file was modified src/HOL/Library/Extended_Nat.thy (diff)
The file was modified src/HOL/Rings.thy (diff)