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

Hi Gottfried,

> 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.

can you give a hint for which sake you are using verbatim?  In LaTeX it
mixes up to purposes

a) interpret source more or less literally

b) present result in typewriter

For each of these, there are different possibilities; especially b) can
be achieved with Isabelle without relying on verbatim.  a) is not so
simple, but there are ways to cope with involving ML (depending how
general it is supposed to be).

> The single ticks aren't looking so good to me at this moment. What I
> need to do is put the different names in the middle of a big paragraph,
> like in these sentences:
>     My dear reader, please consider what happens when /A is'bounded'by
> b/, or
>     My dear reader, please consider what happens when /A is_bounded_by b/.
> It's like recording music. You get up the next morning, and what you
> thought sounded good the night before, doesn't sound so good anymore.
> However, I think camelcase is out, for the most part.

If your primary concern is how identifiers appear in natural language,
you can consider using your specific set of antiquotations where you can
modify identifiers programatically, in the extreme case using an
explicit substitution table.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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