# HG changeset patch
# User wenzelm
# Date 1152040970 -7200
# Node ID dd9decc0bb6d8d9ab9deff58e79fb039817a42a0
# Parent  8d9d770e1f060725c23824eed2108c4a3cf5b4ab
print_facts: all facts;

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.