Summary
- lists form a monoid
- formal passive interpretation proofs for conj and disj
- add monotonicity propertyies of `mult1` and `mult`
- keeping lifting rules local
- epheremal interpretation keeps auxiliary definition localized
- tuned order of declarations and proofs
The file was modified | src/HOL/List.thy (diff) |
The file was modified | src/HOL/Lattices.thy (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |
The file was modified | src/HOL/Analysis/Measure_Space.thy (diff) |
The file was modified | src/HOL/Analysis/Measure_Space.thy (diff) |