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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
