Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: yongjian Li <lyj238@ios.ac.cn>
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!
Email Gateway (Aug 17 2022 at 13:27):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 17 2022 at 13:27):From: Stephan Merz <Stephan.Merz@loria.fr>
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:
Last updated: May 03 2024 at 12:27 UTC