[isabelle-dev] Some proposed extensions to the Isabelle library

[Tobias Nipkow]

Am 21/09/2013 03:08, schrieb Alessandro Coglio:
> 
> I also have a general question about library vs. AFP. There seem to be clear
> cases of things that should go into the library (e.g. new theorems on lists or
> sets) and clear cases of things that should go into the AFP (e.g. a theory of
> context-free grammars). But some cases are less clear to me; for example, while
> lattices are in the library, I noticed that categories are in the AFP (well,
> categories are used much less frequently than lattices, so perhaps that's a
> criterion).

It is not alwasy clear, but your analysis is correct.

> More concretely, I've been working on a couple of developments
> (/not/ included in the attached file) that I can imagine going into either place:
> 
>   * A theory of indexed products, modeled via maps and also modeled via functions.
>   * A theory of ranges over orders/lattices, part of which use the indexed
>     products mentioned above.
> 
> Does anybody have any guidance? Out of curiosity, have theories ever moved
> between library and AFP, in either direction?

It sounds like it is better for the AFP, but when you submit it and we see it we
may feel differently.

Tobias