[isabelle-dev] Fwd: Re: new isabelle interface

[Michael Nedzelsky]

---------------
> I'm thinking about making a new interface to Isabelle, along the lines
> of Proof General, but not requiring Emacs (ugh). It would be done in
> C# and be for Windows initially, though depending on how I do it it
> could probably be made to work in Linux and other Unixen as well.

> First of all, is there anything done already along these lines?

> I plan to use SML.NET to compile Isabelle. Does anyone forsee any
> problems with this? Is Isabelle's code fairly portable across Standard
> ML compilers?

The SML.NET user manual says (p. 4).

"No interactive evaluation. The interactive environment is for compilation
of stand-alone applications or libraries only. SML expressions can not be
evaluated interactively and the use command is not available."

Isabelle sources contains many "use commands", so it will not
run on SML.NET.

> Besides what's in the source distribution, is there any internals
> documentation I should know about?
Yes, I want to know about it too.
There was an attempt to document some internals: see Isabelle Documentation Project
  http://isabelle.in.tum.de/nominal/activities/idp/
But I do not know about any results.

> Chris Capel

  Michael Nedzelsky



---------- Конец пересылаемого письма ----------
-- 
С уважением,
 Michael                          mailto:MichaelNedzelsky at yandex.ru