Re: [isabelle] Multiset elements

Hi René,

Am 21.08.2014 um 13:24 schrieb René Thiemann <rene.thiemann at>:

> if you're going to work on the Multiset-theory, I suggest to add the following four lemmas which might be of general interest:

Thanks. I have just added them to my repository and pushed them to the testboard.

The IsaFoR project seems to have much more to offer in terms of multiset support. If you have other contributions or ideas, please let us know.

Incidentally, the refactoring Dmitriy and I (and Florian) have in mind will probably not happen in the immediate future. We're using multisets in a formalization that we would like to submit to the AFP, so we'd like it to work with both Isabelle2014 and the repository version (as much as possible). Once it's published, we'll start playing with the "Multiset" theory.

Incidentally, our formalization happens to be not too remote from IsaFoR thematically -- our multisets are clauses or collections of clauses in a formalized theorem prover. We'll probably need to talk. ;)



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.