--- a/doc-src/System/fonts.tex Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/System/fonts.tex Mon Aug 28 13:52:38 2000 +0200
@@ -4,8 +4,8 @@
\chapter{Fonts and character encodings}
Using the print mode mechanism of Isabelle, variant forms of output become
-very easy. As the canonical application of this feature, {\Pure} and major
-object-logics (\FOL, \ZF, \HOL, \HOLCF) support optional input and output of
+very easy. As the canonical application of this feature, Pure and major
+object-logics (FOL, ZF, HOL, HOLCF) support optional input and output of
proper mathematical symbols as built-in option.
Symbolic output is enabled by activating the ``\ttindex{symbols}'' print mode.