Re: [isabelle] Juxtaposed cartouche error in session run; okay in PIDE
On Sat, 14 Nov 2015, Gottfried Barrow wrote:
I end this mentioning three "features", some outer syntax commands that
get interpreted as LaTeX newtheorem environments, where the source that
follows is put in a fancyverb environment with line numbers, directly
underneath the newtheorem title. The 3rd feature would be "subtle"
syntax that gets interpreted as a very specific LaTeX equation
I ask, "Do these features exist?", and, "If they don't, should you make
implementing them a priority just for me?"
There is already a "tag" feature that allows to wrap Isabelle document
commands (like 'text') or other formal command (e.g. proof commands) in a
An example can be seen here:
Maybe that is already sufficient to implement all 3 points above.
This archive was generated by a fusion of
Pipermail (Mailman edition) and