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 terms?

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.


	Makarius





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