[isabelle-dev] Proposing extensions to the Isabelle library?

[Tobias Nipkow]

Am 13/12/2012 03:21, schrieb Alessandro Coglio:
> Hello,
> 
> 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.

Thanks
Tobias

> Thank you in advance!
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>