equal
deleted
inserted
replaced
143 * Predefined LaTeX macros for Isabelle symbols \<bind> and \<then> |
143 * Predefined LaTeX macros for Isabelle symbols \<bind> and \<then> |
144 (e.g. see ~~/src/HOL/Library/Monad_Syntax.thy). |
144 (e.g. see ~~/src/HOL/Library/Monad_Syntax.thy). |
145 |
145 |
146 |
146 |
147 *** ML *** |
147 *** ML *** |
|
148 |
|
149 * The inner syntax of sort/type/term/prop supports inlined YXML |
|
150 representations within quoted string tokens. By encoding logical |
|
151 entities via Term_XML (in ML or Scala) concrete syntax can be |
|
152 bypassed, which is particularly useful for producing bits of text |
|
153 under external program control. |
148 |
154 |
149 * Antiquotations for ML and document preparation are managed as theory |
155 * Antiquotations for ML and document preparation are managed as theory |
150 data, which requires explicit setup. |
156 data, which requires explicit setup. |
151 |
157 |
152 * Isabelle_Process.is_active allows tools to check if the official |
158 * Isabelle_Process.is_active allows tools to check if the official |