[isabelle] New AFP theory: List Index

This theory provides functions for finding the index of an element in a
list, by predicate and by value.



Above I have intentionally not used the word "article" but "theory" to
emphasize that this is a small contribution (a single theory of modest
size) - but a reusable one! I would like to use this opportunity to
remind readers of this list of the purpose of the AFP:

"The Archive of Formal Proofs is a collection of proof libraries,
examples, and larger scientific developments."

At the moment the majority of contributions are large (sometimes
impressively so), monolithic developments. Very rarely are parts of such
developments reused elsewhere. That is, the library aspect is
underdeveloped. The above theory "List Index" used to be hidden in the
article "Jinja is not Java" and I have (after 5 years!) finally gotten
around to making it a separate contribution.

This is a call for reusable AFP entries. I am sure many of you have such
theories hidden away in their drawers (or their AFP entries): Do take
the time to polish and submit them to the AFP (or refactor some existing
AFP article), for the benefit of the whole community (and your fame).

	Don't think publication, think reuse!

Sorry about getting carried away ;-)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.