[isabelle-dev] Moving some library material to the AFP

[Lawrence Paulson]

This is a follow-up to a message I sent about a month ago.

We have a couple of real gems hidden among our various examples directories. One of them is an old example of mine, a port of a proof in type theory that Ackermann’s function is not primitive recursive. Another is the construction of the real numbers using Dedekind cuts, which is on the one hand redundant (for some reason another construction of the reals was substituted) but on the other hand iconic (thanks to AUTOMATH).

I think that both of them should be moved to the AFP, and we should look for others. Any other opinions?

Larry