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,


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.