Re: [isabelle] How do I do stone age interaction?



On Wed, 8 Dec 2010, Alexander Krauss wrote:

Maybe for the latter meaning one could read 'Isar' as '*Is*abelle *ar*chitecture'. It was initially introduced to support the language, but it is now central to the whole system.

In other words, the current model is roughly

(4) Isabelle/ML embedded into Isar
--------------------------------------
(3) Isar language
--------------------------------------
(2) Isar infrastructure
--------------------------------------
(1) Raw ML toplevel (provided by compiler)

Very nice explanation -- including all your other text from above that I have suppressed for brevity. I did not know the wording of Isar as *Is*abelle *ar*chitecture' so far.

There is little left to add, apart from (5) Isabelle/Scala and (6) Prover IDE. The latter already helps a lot in exploring Isabelle/ML right now, and at a later stage raw ML access will return for bare bones system maintenance, but that is not very signifant compared to many other things that are still missing.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.