[isabelle-dev] Damn

[Lawrence Paulson]

A slight disappointment this weekend. I thought I would have a proof of the Jordan curve theorem just in time for the release. All the prerequisites seemed to be there. Sledgehammer was proving the goals one after another. Even with the last goal, it proved half and suggested two proofs for the other half. But they didn't work, and a closer look shows that this claim depends on prerequisites involving several thousand lines of HOL Light proof scripts. A bit like the EU-Canada treaty and the Wallonian Parliament.

--lcp