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

author | kleing |

Wed, 18 May 2005 06:29:42 +0200 | |

changeset 15996 | 3699351b8939 |

parent 15995 | 251069032c03 |

child 15997 | c71031d7988c |

documented new thms_containing ('rewrites' still missing)

--- 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}).