[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
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.
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