# 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