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



On Mon, 29 Nov 2010, Burkhart Wolff wrote:

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.

You can try the jEdit-based Prover IDE (PIDE) in Isabelle2009-2 (from the Isabelle download website) by invoking "isabelle jedit" on the command line. Their is also a newer (totally adhoc) snapshot at http://www.lri.fr/~wenzel/Isar2010-Orsay/download.html which makes "Isabelle" start the IDE immediately, without Proof General legacy.

In the next official release we will have both side-by side, but Proof General still the default. It will take quite some time to get such a substantial change from TTY-based proving to full-scale IDE support into everyday practice.


	Makarius





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