doc-src/System/fonts.tex
changeset 9695 ec7d7f877712
parent 7882 52fb3667f7df
child 9984 09fc8fc746c4
     1.1 --- a/doc-src/System/fonts.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/System/fonts.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -4,8 +4,8 @@
     1.4  \chapter{Fonts and character encodings}
     1.5  
     1.6  Using the print mode mechanism of Isabelle, variant forms of output become
     1.7 -very easy. As the canonical application of this feature, {\Pure} and major
     1.8 -object-logics (\FOL, \ZF, \HOL, \HOLCF) support optional input and output of
     1.9 +very easy. As the canonical application of this feature, Pure and major
    1.10 +object-logics (FOL, ZF, HOL, HOLCF) support optional input and output of
    1.11  proper mathematical symbols as built-in option.
    1.12  
    1.13  Symbolic output is enabled by activating the ``\ttindex{symbols}'' print mode.