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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
