Re: [isabelle] detaching sml mode from Prover IDE



Hi Gergely,

> Would it be possible to detach the sml mode of the Prover IDE from
> Isabelle? If one wants to develop in Standard ML, downloading the
> whole Isabelle release is too much of a good thing.

since the SML mode is implemented using the infrastructure of
Isabelle/ML and PIDE itself, there is no economic way to do so.  Of
course you can e.g. strip all the object logic sessions (HOL, FOL, ZF),
but this has no dramatic impact.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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