Re: [isabelle] TLA thoery in src directory



As Larry explained, the TLA theory is an "old-style" theory that was never converted to Isar. It can still be loaded via the legacy mode

Isabelle -P false

I have no plans of converting that theory to Isar. If you are really interested in using TLA with Isabelle, please contact me directly, as I have started encoding TLA+ in Isabelle/Isar.

Kind regards,

Stephan

yongjian Li wrote:
Hi,
    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?

regards!








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