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


        Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to