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