[isabelle-dev] NEWS: embedded YXML syntax

Makarius makarius at sketis.net
Mon Jul 11 17:45:57 CEST 2011

*** 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.

See e.g. Isabelle/0517a69de5d6.


More information about the isabelle-dev mailing list