Dear Tobias, thanks for looking into it.
Thus I would rather not create a growing count_list library, if it can be avoided. Could you try to use the above hint and go via multisets? (I may add one or two of your lemmas anyway, as a compromise)
I will try to replace all my usages of count_list by "count ∘ mset" and see how things turn out.
Cheers, Martin
OpenPGP_0x58AE985FE188789A.asc
Description: OpenPGP public key
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
