Re: [isabelle] Overriding reason not to use single quote or camelcase in identifiers?



On 7/4/2012 4:04 PM, Gottfried Barrow wrote:
SHOW-STOPPER: It's vaguely coming back to me, but I'm pretty sure that the show-stopper was my need for the Verbatim environment. I had to put it in a "text{*...*}" command, but "begin{Verbatim}" and "end{Verbatim}" are picky about what can be on the same line with them. I couldn't get rid of those errors, that I remember.

Anyway, I gave up...

It 's becoming less vague. I could get rid of the compile errors, but because one, or the other, or both \begin{Verbatim} and \end{Verbatim} needed to be on a line with nothing else, I couldn't get rid of the "*}"s, or the "{*"s, or the "(*"s, or the "*)"s. How I was wrapping the Verbatim begin and end, I don't remember, but stars and delimiters were cluttering my document.

But that's to be expected, since I was trying to put all of the Isar code in a verbatim environment, so maybe beginnings and endings on lines by themselves were never a real issue. Ah, I was using the Verbatim gobble feature to gobble up some of the stars and delimiters that wrapped it, but I couldn't gobble them all up.

--GB





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