Re: [isabelle] Isar parser for constant names
On Mon, 19 May 2014, Moa Johansson wrote:
I though I’d make use of the function Parse.const. However, although
this function parses the constant name to a string, it appears it is not
the same one as passing the function names explicitly as a string, which
I would expect.
Parse.const is the right thing, but only half of it, namely the outer
syntax parser. You also need an inners syntax "read" function.
Peeking at the implementation of the 'notation' command suggests the
Proof_Context.read_const ctxt false dummyT
This archive was generated by a fusion of
Pipermail (Mailman edition) and