[isabelle] Re: TLA thoery in src directory



Yes, it is an old development and one of the few that was never converted from ML scripts to Isar scripts. Isabelle can still process the theories, but you can't step through them using Proof General in Isar mode.

There was a Proof General mode for ML scripts, but I'm not certain that it still works, and some configuration is required to switch it on.

Larry Paulson


On 21 Oct 2005, at 04:35, yongjian Li wrote:

    I find that the TLA theory in  src directory is quite strange. It
can not be
processed by Isabelle/Isar.
   Could you please explain sth about  it?







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