Summary
- fixed the proof of pair_measure_count_space
- merged
- fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring
- merged
- type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
The file was modified | src/HOL/Analysis/Binary_Product_Measure.thy (diff) |
The file was modified | src/HOL/Library/Extended_Nonnegative_Real.thy (diff) |
The file was modified | src/HOL/Nat.thy (diff) |
The file was modified | src/HOL/Library/Extended_Nat.thy (diff) |
The file was modified | src/HOL/Rings.thy (diff) |