On Wed, 18 Jan 2012, Alexander Krauss wrote:
On 01/18/2012 03:34 PM, Ondřej Kunčar wrote:
It's a bit annoying if you want to do
debugging on the ML level and you have to inspect every term by
inspecting its ML representation (which is really tedious for larger
terms).
This is a common problem, and everybody has come up with private hacks.
Mine goes roughly like this:
Meta-Answer: This is a perfectly normal isabelle-users question.
ML has always been part of the regular Isabelle user space. In ancient
times every proof script was in ML. When I introduced the Isabelle/Isar
toplevel, its very first command was 'ML' to re-integrate the runtime
compilation-execution that is so important for many Isabelle applications.
(Paradoxically, serious Isabelle/ML integration really started with the
Isar toplevel.)
The isabelle-dev mailing list is mainly for things relevant to the process
around the repository and administrative issues (isatest, mira etc.).
For postings related to repository versions one always needs to quote a
proper changeset id so that things can be followed days/weeks/months later
(we have more than 46245 "current" Isabelle versions now, as of
Isabelle/9f39ae84b593, and in a distributed setting there is not global
tip version anyway.)
In contrast, things posted on isabelle-users can usually refer implicitly
to "the latest" official release. In the worst case one merely has to try
1-3 latests official releases. So users don't have to be tought how to
quote versions.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
