| Hello, The attached file contains a fairly heterogeneous collection of potential extensions to the Isabelle library, which I've been developing as part of some projects that I'm working on. I think that other Isabelle users may find them useful. Please let me know if you'd rather receive these in smaller chunks, if anything needs more explanations, if anything should be changed to conform to Isabelle library styles/conventions, etc. 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). 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:
Does anybody have any guidance? Out of curiosity, have theories ever moved between library and AFP, in either direction? Thank you in advance and best regards. |
ProposedLibraryExtensions.thy
Description: Binary data
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
