[isabelle] How do I retrieve the mixfix syntax of a constant?
Dear Isabelle Users and Gurus,
I have written a ML function which creates a new constant definition
based on the type of an old one, for example, the _any transform:
"map_bp_any p ≡ λs. ∃v. map_bp p v s"
(where map_bp was also defined using "definition")
I also want to generate the appropriate mixfix syntax for the new
constant. I know how to do the transformation and how to declare syntax,
but I need to get the syntax for a constant, e.g. "map_bp". I've been
grepping through the source but can't see anything that returns a mixfix.
In this case, I want to get out:
("_ :→ _" [56,51] 56)
so I can turn it into:
("_ :→ -"  56)
Does anyone know how to do the syntax retrieval for a constant?
This archive was generated by a fusion of
Pipermail (Mailman edition) and