Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. lists form a monoid
  2. formal passive interpretation proofs for conj and disj
  3. add monotonicity propertyies of `mult1` and `mult`
  4. keeping lifting rules local
  5. epheremal interpretation keeps auxiliary definition localized
  6. tuned order of declarations and proofs
Changeset 63662:5cdcd51a4dad by haftmann:
lists form a monoid
The file was modified src/HOL/List.thy (diff)
Changeset 63661:92e037803666 by haftmann:
formal passive interpretation proofs for conj and disj
The file was modified src/HOL/Lattices.thy (diff)
Changeset 63660:76302202a92d by bertram felgenhauer _bertram.felgenhauer@uibk.ac.at_:
add monotonicity propertyies of `mult1` and `mult`
The file was modified src/HOL/Library/Multiset.thy (diff)
Changeset 63659:abe0c3872d8a by haftmann:
keeping lifting rules local
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 63658:7faa9bf9860b by haftmann:
epheremal interpretation keeps auxiliary definition localized
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
Changeset 63657:3663157ee197 by haftmann:
tuned order of declarations and proofs
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)