Re: [isabelle] How to use latex commands inside proof?



On Wed, 10 Sep 2014, W. Douglas Maurer wrote:

I can't figure out "Volume 110, Issue 40", which is probably just a private numbering by the mailing list server due to your subscription, which is presumably in "digest" mode.

Can you point out the concrete problem again?

Here is what Holden Lee wrote:
"I'd like to put in some comments like so:
proof -
...
-- "some typeset math here like $a \in A$"
...
but it seems like \ can't be used, and \\ doesn't escape it. What's the
correct way?

That was the thread "How to use latex commands inside proof?" from August 2014. It was answered exhaustively by Andreas Lochbihler and myself, e.g. see here https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-August/msg00257.html


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.