[isabelle-dev] NEWS: embedded YXML syntax

[Alexander Krauss]

On 07/11/2011 05:45 PM, Makarius wrote:
> *** ML ***
>
> * The inner syntax of sort/type/term/prop supports inlined YXML
> representations within quoted string tokens. By encoding logical
> entities via Term_XML (in ML or Scala) concrete syntax can be
> bypassed, which is particularly useful for producing bits of text
> under external program control.

I'm having trouble understanding this... Do you have an example / 
intended use?

Thanks,
Alex