diff -r 8d9d770e1f06 -r dd9decc0bb6d doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Tue Jul 04 19:49:59 2006 +0200 +++ b/doc-src/IsarRef/pure.tex Tue Jul 04 21:22:50 2006 +0200 @@ -1584,8 +1584,8 @@ \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts, using Isabelle's graph browser tool (see also \cite{isabelle-sys}). -\item [$\isarkeyword{print_facts}$] prints any named facts of the current - context, including assumptions and local results. +\item [$\isarkeyword{print_facts}$] prints all local facts of the + current context, both named and unnamed ones. \item [$\isarkeyword{print_binds}$] prints all term abbreviations present in the context.