[isabelle-dev] Isabelle and AFP

Peter Gammie peteg42 at gmail.com
Fri Aug 26 12:43:44 CEST 2011


Amongst the set/pred emails this one doesn't seem to have garnered much response:

On 17/08/2011, at 9:18 PM, Florian Haftmann wrote:

> I repeatedly stumble over duplication among the Isabelle distribution
> and the AFP [..]

I too would be keen to see some way of moving reusable (especially small) parts of AFP entries into Isabelle proper. Typically I need a few minor lemmas that make me wonder if everyone else has proved them already...

Concretely we see this presently with the saturated naturals theory that you want me to clean up. (Soon, I hope. :-)


More information about the isabelle-dev mailing list