Re: [isabelle] How do I do stone age interaction?
On Sun, 28 Nov 2010, mark at proof-technologies.com wrote:
These documents I'm sure will be very useful, and Makarius's
implementation manual looks especially useful for my purposes. But I
also want to carry out basic interaction - this is just the way I go
about learning about the innards of a system - I like to construct my
own terms and experiment. So can I enter HOL term quotations in
Isabelle 2005? And can I use ML constructor functions to create HOL
The most productive way to do this is to use Isabelle2009-2 with
Isabelle/jEdit, which happens to be part of that distribution as sneak
preview. You can then use it as simple "IDE" for ML: it provides tooltips
for inferred ML types and hyperlinks to the sources (using CONTROL/COMMAND
with mouse hovering).
In the next release this mode of interaction will work even more smoothly.
At some later stage I might also provide a raw ML console for the
low-level tinkering below Isabelle itself, but that is a different story.
This archive was generated by a fusion of
Pipermail (Mailman edition) and