equal
deleted
inserted
replaced
692 the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an |
692 the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an |
693 appropriate path specification for {\TeX} inputs. |
693 appropriate path specification for {\TeX} inputs. |
694 |
694 |
695 If the text contains any references to Isabelle symbols (such as |
695 If the text contains any references to Isabelle symbols (such as |
696 \verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well. This package |
696 \verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well. This package |
697 contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, (see \appref{app:symbols} for a |
697 contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, see \cite{isabelle-implementation} for a |
698 complete list of predefined Isabelle symbols). Users may invent |
698 complete list of predefined Isabelle symbols. Users may invent |
699 further symbols as well, just by providing {\LaTeX} macros in a |
699 further symbols as well, just by providing {\LaTeX} macros in a |
700 similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabellesym{\isachardot}sty}}}} of |
700 similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabellesym{\isachardot}sty}}}} of |
701 the distribution. |
701 the distribution. |
702 |
702 |
703 For proper setup of DVI and PDF documents (with hyperlinks and |
703 For proper setup of DVI and PDF documents (with hyperlinks and |