[isabelle-dev] From name string to Sledgehammer_Fact.fact_override

[Albert Jiang]

Hello,

I wish to write an ML function that does the following: transform the name
of a fact to (Facts.ref * Token.src list) such that it can be used as part
of Sledgehammer_Fact.fact_override.

The requirement arises from the need to translate the command e.g.,
"sledgehammer (del: one_add_one)" in Isabelle/jEdit to Isabelle/ML. I only
have the name of the fact but not its proper representation for
Sledgehammer fact_override. I tried to look at what the parser does but
cannot decipher its behaviour. Therefore I would greatly appreciate a
succinct function that does the transformation specified above.

Many thanks,
Albert
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20221110/5092216e/attachment.htm>