--- a/doc-src/TutorialI/Documents/document/Documents.tex Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Wed Jun 22 09:26:18 2005 +0200
@@ -656,8 +656,8 @@
parsing and type-checking. Document preparation enables symbolic
output by default.
- \medskip The next example includes an option to modify Isabelle's
- \verb,show_types, flag. The antiquotation
+ \medskip The next example includes an option to show the type of all
+ variables. The antiquotation
\texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
output \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Type inference has figured
out the most general typings in the present theory context. Terms