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



Dear Larry,



Am 29.11.2010 um 12:49 schrieb Lawrence Paulson:

> I must give this a try sometime. Does even the standard version of jEdit have this ML mode?

What do you mean exactly ?

You certainly know the ML-environment in Default-ISAR:

ML{*
fun fac x = if x = 0 then 1 else x * fac(x-1)
*}

If you use jEdit, and press the shift- button while hovering,
for example, over the "x" in the ML code, you get directly
type "int" in the display. Makarius demonstrated this already
in the Isabelle developper days in Cambridge, but it may well 
be that you missed this session.

It is planned that future versions of jEdit (which we will call Pide
in the future because thats the project that finances Makarius
work here) will do that for any part of inner syntax.

Hhm, I intended to send my mail to Isabelle-users - in case I 
adressed this only to you, could you please forward it ?

bu


> Larry
> 
> On 29 Nov 2010, at 08:25, Burkhart Wolff wrote:
> 
>> Hmm, i'm one of these dinosaurs that program Isabelle on the ml - level myself. These days, I'll do that inside isar in the ML{} environment which is, I believe, now the best ml environment out there - in jEdit, you can even hover over ml expressions and get the type information. It speeds up ml development even if you do not even target isabelle. You can even try to program without antiquotations, sometimes this is instructive to see what they actually do. However, since they offer a certain infra-structure and discipline to handle proof and theory contexts, they help to avoid the common error to reuse a stale context, which the kernel must avoid in order to become a purely functional transaction machine.
> 






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