Re: [isabelle] antiquotations

Hi Makarius,

Thanks - what I really meant when I asked about documentation was, how do I find out how to get the goal as an ML value when I don't already know the answer to that question. I agree that if I know the answer then it's easy to find it in the canonical documentation.

In fact the preceding section in the Implementation manual is about the Proof structure, which also looks as though it contains useful stuff, except that one needs to get hold of the current proof state. How do you get the current proof state as an ML value?

Thanks for the pointer about apply tactic ..., yes it's possible to write a tactic which does nothing but print out the goal, and can use the goal as an ML value within the tactic, but when I tried to define a reference value in which to save the goal value I found I couldn't. Has the version of ML available to Isar users been jinxed, or something, so that reference variables don't work?

For your information, I don't want to recreate the look-and-feel of
(what you now, I think correctly, admit is a) different system called "Isabelle98". I just want to get stuff done. The sort of stuff (like finding out how to get hold of the current goal) that takes no time at all in HOL4 or Isabelle2005 (which is actually what I use when I'm building on previous work) and takes hours in your Isabelle 2017

Incidentally, on the subject of documentation - what about the Isabelle cookbook - why isn't it included as part of the Isabelle documentation (and kept up to date)?



On 05/06/18 01:14, Makarius wrote:
On 04/06/18 16:52, Dominique Unruh wrote:
I don't know if it's documented. I found it via autocompletion in
Isabelle/jEdit. But it took some experimenting to figure out that it works
with ML_val. (Because otherwise it just thrown UNDEF).

The canonical documentation for Isabelle/ML is the "implementation"
manual. You can look at the index for Isar.goal or use Isabelle/jEdit to
make a hypersearch for it on all documentation sources:
$ISABELLE_HOME/src/Doc -- the latter gives a "live" view on that
document (including example snippets) in the Prover IDE.

Anyway, I suspect that Jeremy wants to recreate the look-and-feel of
different system called "Isabelle98" from 20 years ago. For that, the
proof method called "tactic" might help: it is documented in the
"isar-ref" manual, section "7.3: Tactics -- improper proof methods".
This already indicates that we are looking at fringe topics of Isabelle2017.


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