Stream: Mirror: Isabelle Development Mailing List

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

view this post on Zulip Email Gateway (Mar 03 2022 at 14:45):

From: 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?


isabelle-dev mailing list

Last updated: Feb 24 2024 at 04:17 UTC