[isabelle-dev] NEWS: embedded YXML syntax

Alexander Krauss krauss at in.tum.de
Mon Jul 11 18:33:14 CEST 2011

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?


More information about the isabelle-dev mailing list