summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 22 May 2005 16:51:05 +0200 | |

changeset 16017 | cb983795bcdf |

parent 16016 | 9e57d19cb21c |

child 16018 | 3e4e077af2e7 |

tuned thms_containing;

--- a/doc-src/IsarRef/pure.tex Sun May 22 16:51:04 2005 +0200 +++ b/doc-src/IsarRef/pure.tex Sun May 22 16:51:05 2005 +0200 @@ -1434,11 +1434,10 @@ \railterm{thmdeps} \begin{rail} - thmscontaining (('(' nat ')')?) ((criterion '-'?) * ) - % no idea why this needs to be backwards (should be '-'? criterion), - % but it comes out right this way + thmscontaining (('(' nat ')')?) (criterion *) ; - criterion: 'intro' | 'elim' | 'dest' | 'term' | 'name' ':' string + criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | + 'rewrite' ':' term | term) ; thmdeps thmrefs ; @@ -1472,19 +1471,20 @@ packages, such as $\isarkeyword{datatype}$. \item [$\isarkeyword{thms_containing}~\vec c$] retrieves facts from the theory - or proof context matching all of the search criteria $\vec c$. The - criteria $\isarkeyword{intro}$, $\isarkeyword{elim}$, and - $\isarkeyword{dest}$ select theorems that match the current goal as - introduction, elimination or destruction rules respectively. The - criterion $\isarkeyword{name}$ $:$ $s$ selects all theorems that - contain $s$ in their fully qualified name and the criterion which - consists of any term $t$ selects theorems that contain the pattern - $t$, which may contain occurrences of ``$\_$'' as well as type - restrictions. 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. + or proof context matching all of the search criteria $\vec c$. A criterion + $name: s$ selects all theorems that contain $s$ in their fully qualified + name. The criteria $intro$, $elim$, and $dest$ select theorems that match + the current goal as introduction, elimination or destruction rules, + respectively. A criterion $rewrite: t$ selects all rewrite rules whose + left-hand side matches the given term. A criterion term $t$ selects all + theorems that contain the pattern $t$ -- as usual patterns may contain + occurrences of the dummy ``$\_$'', schematic variables, and type + constraints. + + 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. \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts, using Isabelle's graph browser tool (see also \cite{isabelle-sys}).