Email Gateway (Aug 18 2022 at 14:41): Email Gateway (Aug 18 2022 at 14:41):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
In a recent off-line discussion is was suggested that the notation of
the two orderings in HOL/Library/Multiset.thy should be swapped, i.e.
< -- the pointwise ordering
<# -- the multiset order
This would establish a closer correspondence to ordinary sets and allow
us to use more type classes from the orderings / lattices hierarchy.
Any comments or objections?
Florian
signature.asc
Last updated: Apr 26 2024 at 20:16 UTC