Re: [isabelle] antiquotations

On 05/06/18 04:12, Jeremy Dawson wrote:
> 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?

E.g. like this:

lemma "x = x"
  ML_val ‹@{Isar.goal}›
  ML_val ‹Toplevel.proof_of @{Isar.state}›

This has little practical relevance though. We are merely toying around
with details of the implementation here.

> 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?

Isabelle/ML is a very clean parallel programming environment, as
explained in chapter 0 of the "implementation" manual. Section 0.7.9 is
about Usynchronitzed.ref and Section 0.8 about "Thread-safe programming".

> 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

In Isabelle you have the goal right there in the source, and the Prover
IDE manages proof documents that apply to it. Anything beyond that is
for tool developers, and even that is quite easy if you think about the
system in the proper way, and look a bit through the documentation.

Note that "to get stuff done" (doing proofs) usually requires no
Isabelle/ML at all.


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