Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. use the cancellation simprocs directly
  2. don't activate simproc on cancel_comm_monoid_add
Changeset 65031:52e2c99f3711 by fleury _mathias.fleury@mpi-inf.mpg.de_:
use the cancellation simprocs directly
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Multiset_Order.thy (diff)
The file was removedsrc/HOL/Library/multiset_order_simprocs.ML
Changeset 65030:7fd4130cd0a4 by fleury _mathias.fleury@mpi-inf.mpg.de_:
don't activate simproc on cancel_comm_monoid_add
The file was modified src/HOL/Library/Cancellation.thy (diff)