Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] From name string to Sledgehammer_Fact.fact...

view this post on Zulip Email Gateway (Nov 10 2022 at 10:51):

From: Albert Jiang <>

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,

Last updated: Mar 04 2024 at 10:08 UTC