[isabelle] A few questions about LaTeX theory output



I'm having a few problems formatting my theory.

- Is there a way to make syntax appear for an arbitrary definition
without changing the each use?  I thought "notation" would do this,
but my typesetting didn't change.

  For example, can I issue a command at the top of my theory that will
change "card A" into "|A|" in LaTeX output, without having to change
every occurrence of "card A" into something else?

  Also, can I still do this (e.g. for a binary function constant) even
if there is no associated ASCII infix syntax for it?

- Importing LaTeXsugar and OptionalSugar into my theory didn't seem to
change anything.  In particular, e.g., "\<not>(\<exists M. ...)" does
not produce the the exists symbol with a slash through it, as the
"sugar for LaTeX documents" pdf [0] says it should; it produces what
"\<not>(\<exists> M. ...)" would produce normally.  As another
example, the empty set is still typeset as "{}".  (I added a
\usepackage{amssymb} to root.tex as indicated by "sugar...".)



[0] http://isabelle.in.tum.de/dist/Isabelle/doc/sugar.pdf

-- 
 Denis





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