# HG changeset patch
# User kleing
# Date 1171927438 -3600
# Node ID 306488144b4ada7fbfb87c835704524f0debfc8f
# Parent  275802767bf3e20b3674c6701d5a8d0b12aae1c0
updated docs with new with_dups syntax for find_theorems

diff -r 275802767bf3 -r 306488144b4a doc-src/IsarRef/pure.tex
--- 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}).