# HG changeset patch # User kleing # Date 1116390582 -7200 # Node ID 3699351b89394174f8ed58bd45a37e969013a89a # Parent 251069032c031c038ac4eb1f1a96a9d0d8ca4bd4 documented new thms_containing ('rewrites' still missing) diff -r 251069032c03 -r 3699351b8939 doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Wed May 18 00:13:19 2005 +0200 +++ b/doc-src/IsarRef/pure.tex Wed May 18 06:29:42 2005 +0200 @@ -1434,7 +1434,11 @@ \railterm{thmdeps} \begin{rail} - thmscontaining ('(' nat ')')? (term * ) + thmscontaining (('(' nat ')')?) ((criterion '-'?) * ) + % no idea why this needs to be backwards (should be '-'? criterion), + % but it comes out right this way + ; + criterion: 'intro' | 'elim' | 'dest' | 'term' | 'name' ':' string ; thmdeps thmrefs ; @@ -1467,11 +1471,19 @@ transaction; this allows to inspect the result of advanced definitional packages, such as $\isarkeyword{datatype}$. -\item [$\isarkeyword{thms_containing}~\vec t$] retrieves facts from the theory - or proof context containing all of the constants or variables occurring in - terms $\vec t$ (which may contain occurrences of ``$\_$''). Note that - giving the empty list yields \emph{all} currently known facts. An optional - limit for the number printed facts may be given; the default is 40. +\item [$\isarkeyword{thms_containing}~\vec c$] retrieves facts from the theory + or proof context matching all of the search criteria $\vec c$. Valid + criteria are $\isarkeyword{intro}$, $\isarkeyword{elim}$, and + $\isarkeyword{dest}$, selecting theorems that match the current goal + as introduction, elimination or destruction rules respectively, + $\isarkeyword{name}$ $:$ $s$, selecting all theorems that contain + $s$ in their fully qualified name, and finally any term $t$ which + may contain occurrences of ``$\_$'' and type restrictions, selecting + theorems that contain the pattern $t$. Criteria can be preceded by + \texttt{-} 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. \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts, using Isabelle's graph browser tool (see also \cite{isabelle-sys}).