# HG changeset patch
# User wenzelm
# Date 1378814569 -7200
# Node ID abec1d118bc9339706cda118c8a12d0def2f5788
# Parent  05313b45a5aef17abfd53750e879ccf648219d8c
tuned;

diff -r 05313b45a5ae -r abec1d118bc9 src/Doc/IsarRef/Misc.thy
--- a/src/Doc/IsarRef/Misc.thy	Tue Sep 10 11:57:53 2013 +0200
+++ b/src/Doc/IsarRef/Misc.thy	Tue Sep 10 14:02:49 2013 +0200
@@ -46,7 +46,7 @@
   \begin{description}
   
   \item @{command "print_theory"} prints the main logical content of
-  the theory context; the ``@{text "!"}'' option indicates extra
+  the background theory; the ``@{text "!"}'' option indicates extra
   verbosity.
 
   \item @{command "print_methods"} prints all proof methods
@@ -55,8 +55,9 @@
   \item @{command "print_attributes"} prints all attributes
   available in the current theory context.
   
-  \item @{command "print_theorems"} prints theorems resulting from the
-  last command; the ``@{text "!"}'' option indicates extra verbosity.
+  \item @{command "print_theorems"} prints theorems of the background
+  theory resulting from the last command; the ``@{text "!"}'' option
+  indicates extra verbosity.
   
   \item @{command "find_theorems"}~@{text criteria} retrieves facts
   from the theory or proof context matching all of given search