--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Sep 24 15:56:29 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Sep 24 16:17:59 2010 +0200
@@ -266,8 +266,8 @@
\item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
- \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a type constructor
- (logical or abbreviation) \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
+ \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a (logical or syntactic) type
+ constructor \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
\item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}class\ c{\isacharbraceright}{\isachardoublequote}} prints a class \isa{c}.