[isabelle-dev] Proposing extensions to the Isabelle library?
nipkow at in.tum.de
Thu Dec 13 10:24:51 CET 2012
Am 13/12/2012 03:21, schrieb Alessandro Coglio:
> Is there a process to propose extensions to the Isabelle library? Is
> isabelle-dev the right place, as opposed to isabelle-users?
> As part of an Isabelle project, I've developed some type classes and theorems
> for orders and lattices (see attached file) that could be of general use.
I looked at your theory, which deals with orderings on product types, and
noticed a few things:
1. We already have Library/Product_ord, but it defines a *lexicographic*
ordering. Any objections if we rename it to Lex_Product_ord?
2. We also have a Library/Product_lattice. It covers much the same ground as
your LibExt. I would not want to add another similar theory, but if you have any
additional results not contained in Product_lattice already, please filter them
out and I can add them.
> Thank you in advance!
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev