# HG changeset patch # User lcp # Date 799512377 -7200 # Node ID a203181678d3a9d76bf5fd6cd30dc613d06c5caf # Parent b9594fe65d89507ec8af426a61fe4108ba7e0daf show_sorts:=true forces display of types diff -r b9594fe65d89 -r a203181678d3 doc-src/Ref/introduction.tex --- a/doc-src/Ref/introduction.tex Wed May 03 16:30:39 1995 +0200 +++ b/doc-src/Ref/introduction.tex Wed May 03 16:46:17 1995 +0200 @@ -158,8 +158,8 @@ makes Isabelle show types when printing a term or theorem. \item[\ttindexbold{show_sorts} := true;] -makes Isabelle show the sorts of type variables. It has no effect unless -{\tt show_types} is~{\tt true}. +makes Isabelle show both types and the sorts of type variables. It does not +matter whether {\tt show_types} is also~{\tt true}. \end{ttdescription}