(*<*) theory find2 imports Main begin lemma"A ∧ B" (*>*)
txt‹\index{finding theorems}\index{searching theorems} In
S\ref{sec:find}, we introduced Proof General's \pgmenu{Find} button
finding theorems in the database via pattern matching. If we are
a proof, we can be more specific; we can search for introduction,
and destruction rules \emph{with respect to the current goal}.
this purpose, \pgmenu{Find} provides three aditional search criteria:
texttt{intro}, \texttt{elim} and \texttt{dest}.
example, given the goal @{subgoals[display,indent=0,margin=65]}
can click on \pgmenu{Find} and type in the search expression
texttt{intro}. You will be shown a few rules ending in ‹==> ?P ∧ ?Q›,
them @{thm[source]conjI}\@. You may even discover that
very theorem you are trying to prove is already in the
. Given the goal› (*<*) oops lemma"A ⟶ A" (*>*) txt‹\vspace{-\bigskipamount}
{subgoals[display,indent=0,margin=65]}
search for \texttt{intro} finds not just @{thm[source] impI}
also @{thm[source] imp_refl}: @{thm imp_refl}.
before, search criteria can be combined freely: for example,
begin{ttbox}
_ \at\ _" intro
end{ttbox}
for all introduction rules that match the current goal and
the ‹@› function.
for elimination and destruction rules via \texttt{elim} and
texttt{dest} is analogous to \texttt{intro} but takes the assumptions
account, too. › (*<*) oops end (*>*)
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet am 2026-06-29)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
