[isabelle-dev] From name string to Sledgehammer_Fact.fact_override
albert594250 at gmail.com
Thu Nov 10 11:49:55 CET 2022
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
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev