doc-src/IsarRef/Thy/document/Document_Preparation.tex
changeset 39689 78b185bf7660
parent 39437 8c23c61c6d5c
child 40255 9ffbc25e1606
     1.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Sep 24 15:56:29 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Sep 24 16:17:59 2010 +0200
     1.3 @@ -266,8 +266,8 @@
     1.4  
     1.5    \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
     1.6  
     1.7 -  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a type constructor
     1.8 -    (logical or abbreviation) \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
     1.9 +  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a (logical or syntactic) type
    1.10 +    constructor \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
    1.11  
    1.12    \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}class\ c{\isacharbraceright}{\isachardoublequote}} prints a class \isa{c}.
    1.13