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

Tobias Nipkow nipkow at in.tum.de
Tue Sep 24 14:25:09 CEST 2013

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.


More information about the isabelle-dev mailing list