[isabelle-dev] Isabelle and AFP

[Peter Gammie]

Florian,

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. :-)

cheers
peter