Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2020-RC1 --- Prover IDE support for Po...

Email Gateway (Aug 23 2022 at 08:41):

From: Makarius <makarius@sketis.net>
Here is just one particularly interesting item from
https://isabelle.in.tum.de/website-Isabelle2020-RC1/dist/Isabelle2020-RC1/doc/NEWS.html

* ML *

• Prover IDE support for the underlying Poly/ML compiler (not the basis
  library). Open $ML_SOURCES/ROOT.ML in Isabelle/jEdit to browse the
  implementation with full markup.

It is fun to browse this great software product by David Matthews with full
IDE markup. An excellent example for the principle of self-application /
self-hosting of the Isabelle platform.

Makarius

Last updated: Apr 26 2024 at 12:28 UTC