--- a/doc-src/IsarRef/pure.tex Tue Feb 20 00:14:33 2007 +0100
+++ b/doc-src/IsarRef/pure.tex Tue Feb 20 00:23:58 2007 +0100
@@ -1528,7 +1528,7 @@
'print\_theory' ( '!'?)
;
- 'find\_theorems' (('(' nat ')')?) (criterion *)
+ 'find\_theorems' (('(' nat ')')?) ('with_dups')? (criterion *)
;
criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
'simp' ':' term | term)
@@ -1581,7 +1581,8 @@
Criteria can be preceded by ``$-$'' to select theorems that do \emph{not}
match. Note that giving the empty list of criteria yields \emph{all}
currently known facts. An optional limit for the number of printed facts
- may be given; the default is 40.
+ may be given; the default is 40. Per default, duplicates are removed from
+ the search result. Use $\isarkeyword{with_dups}$ to display duplicates.
\item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
using Isabelle's graph browser tool (see also \cite{isabelle-sys}).