On 27/07/2016 11:39, Jasmin Blanchette wrote:
Tobias wrote:
Did we ever discuss the naming issue? "insert_mset" would be the canonical
name, but it would make larger expressions hard to read.
I'm not so sure "insert_mset" would be the right name. Its set-based
terminology might suggest a
Tobias wrote:
> Did we ever discuss the naming issue? "insert_mset" would be the canonical
> name, but it would make larger expressions hard to read.
I'm not so sure "insert_mset" would be the right name. Its set-based
terminology might suggest a definition like
insert_mset x M = {#x#} #∪
Naming: can't we drop "is_"?
Tobias
On 27/07/2016 10:46, Manuel Eberl wrote:
*** HOL ***
* Number_Theory: algebraic foundation for primes: Introduction of
predicates "is_prime", "irreducible", a "prime_factorization"
function, the "factorial_ring" typeclass with instance proofs for
nat, int, p
*** HOL ***
* Number_Theory: algebraic foundation for primes: Introduction of
predicates "is_prime", "irreducible", a "prime_factorization"
function, the "factorial_ring" typeclass with instance proofs for
nat, int, poly.
* Probability: Code generation and QuickCheck for Probability Mass
Functio
> On 27 Jul 2016, at 08:00, Tobias Nipkow wrote:
>
> No, we keep talking about it (internally), but nobody at TUM has done
> anything about it. It would be great if you want to take this on. It is
> potentially tedious because there are many existing uses of multisets.
Indeed, it will probabl
