Re: [isabelle] antiquotations

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.