doc-src/Ref/introduction.tex
changeset 1102 a203181678d3
parent 884 35c836adf48f
child 1372 16330e3fa3b7
equal deleted inserted replaced
1101:b9594fe65d89 1102:a203181678d3
   156 
   156 
   157 \item[\ttindexbold{show_types} := true;]
   157 \item[\ttindexbold{show_types} := true;]
   158 makes Isabelle show types when printing a term or theorem.
   158 makes Isabelle show types when printing a term or theorem.
   159 
   159 
   160 \item[\ttindexbold{show_sorts} := true;]
   160 \item[\ttindexbold{show_sorts} := true;]
   161 makes Isabelle show the sorts of type variables.  It has no effect unless
   161 makes Isabelle show both types and the sorts of type variables.  It does not
   162 {\tt show_types} is~{\tt true}. 
   162 matter whether {\tt show_types} is also~{\tt true}. 
   163 \end{ttdescription}
   163 \end{ttdescription}
   164 
   164 
   165 
   165 
   166 \subsection{$\eta$-contraction before printing}
   166 \subsection{$\eta$-contraction before printing}
   167 \begin{ttbox} 
   167 \begin{ttbox}