Re: [isabelle-dev] Multiset insert

2016-07-28 Thread Jasmin Blanchette
> On 28.07.2016, at 10:33, Peter Lammich wrote: > >>> How about >>> >>> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where >>> "add# x M = {#x#} + M" > > This, however, may produce confusion with multiset union, which is an > instance of the plus type

Re: [isabelle-dev] Multiset insert

2016-07-28 Thread Tobias Nipkow
On 28/07/2016 10:33, Peter Lammich wrote: On Do, 2016-07-28 at 10:21 +0200, Jasmin Blanchette wrote: Tobias wrote: How about definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where "add# x M = {#x#} + M" This, however, may produce confusion with multiset union, which is an

Re: [isabelle-dev] Multiset insert

2016-07-28 Thread Manuel Eberl
I've been using multisets quite a bit myself lately. add# and add1# both sound all right to me. I would also like to point out that for some reason, intersection and union are #∪ and #∩, whereas all other multiset operations seem to have the # at the end (e.g. ⊆#). Unless there is some deeper

Re: [isabelle-dev] Multiset insert

2016-07-28 Thread Tobias Nipkow
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

Re: [isabelle-dev] Multiset insert

2016-07-28 Thread Peter Lammich
On Do, 2016-07-28 at 10:21 +0200, Jasmin Blanchette wrote: > Tobias wrote: > > > How about > > > > definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where > > "add# x M = {#x#} + M" This, however, may produce confusion with multiset union, which is an instance of the plus type

Re: [isabelle-dev] Multiset insert

2016-07-28 Thread Jasmin Blanchette
Tobias wrote: > How about > > definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where > "add# x M = {#x#} + M" Lovely! Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Multiset insert

2016-07-28 Thread Florian Haftmann
>> Tobias wrote: >> >>> How about >>> >>> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where >>> "add# x M = {#x#} + M" > > This, however, may produce confusion with multiset union, which is an > instance of the plus type classes, i.e., occupying the name > plus_multiset. To

Re: [isabelle-dev] Multiset insert

2016-07-28 Thread Florian Haftmann
Just an aside: concerning »insert« and »add«, infix syntax would be desirable, e.g. a `insert` X a `add` M similar to Y \union Y N + M which would yield much more readable propositions, esp. wrt. associativity: a `insert` b `insert` X = {a, b} \union X

Re: [isabelle-dev] Multiset insert

2016-07-28 Thread Jasmin Blanchette
> I would also like to point out that for some reason, intersection and union > are #∪ and #∩, whereas all other multiset operations seem to have the # at > the end (e.g. ⊆#). Unless there is some deeper reason for this, I suggest we > change it. Good point. Indeed, I first wrote ∪# in

Re: [isabelle-dev] NEWS: Primes

2016-07-28 Thread Manuel Eberl
Yes, that might be a good idea. On 27/07/16 11:24, Tobias Nipkow wrote: 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"

[isabelle-dev] jdk-8u102

2016-07-28 Thread Makarius
With Isabelle/e506baad44fa we are on jdk-8u102, which is a recent update by Oracle with a lot of changes. See also http://www.oracle.com/technetwork/java/javase/8u102-relnotes-3021767.html http://www.oracle.com/technetwork/java/javase/2col/8u102-bugfixes-3021768.html Occording to my