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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev