*** Prover IDE -- Isabelle/Scala/jEdit ***
* IDE support for the Isabelle/Pure bootstrap process, with the
following independent stages:
src/Pure/ROOT0.ML
src/Pure/ROOT.ML
src/Pure/Pure.thy
src/Pure/ML_Bootstrap.thy
The ML ROOT files act like quasi-theories in the context of theory
On Thu, 7 Apr 2016, Makarius wrote:
*** Prover IDE -- Isabelle/Scala/jEdit ***
* IDE support for the Isabelle/Pure bootstrap process.
After further refinements (e.g. see current Isabelle/79f41fbdf74a), the
Pure IDE bootstrap works even more smoothly. In particular it can be
combined with
On Thu, 7 Apr 2016, Makarius wrote:
Maybe some other big applications of Poly/ML should be made
PIDE-compliant as well, e.g. HOL4 or even Poly/ML itself.
Or maybe even this one: https://bitbucket.org/lcpaulson/metitarski
Makarius
___
*** Prover IDE -- Isabelle/Scala/jEdit ***
* IDE support for the Isabelle/Pure bootstrap process. The file
src/Pure/ROOT.ML may be opened with Isabelle/jEdit: it acts like a
theory body in the context of theory ML_Bootstrap. This allows
continuous checking of ML files as usual, but the result is
