src/Doc/Tutorial/Rules/find2.thy

+(*<*)
+theory find2 imports Main begin
+lemma "A \<and> B"
+(*>*)
+
+txt{*\index{finding theorems}\index{searching theorems} In
+\S\ref{sec:find}, we introduced Proof General's \pgmenu{Find} button
+for finding theorems in the database via pattern matching. If we are
+inside a proof, we can be more specific; we can search for introduction,
+elimination and destruction rules \emph{with respect to the current goal}.
+For this purpose, \pgmenu{Find} provides three aditional search criteria:
+\texttt{intro}, \texttt{elim} and \texttt{dest}.
+
+For example, given the goal @{subgoals[display,indent=0,margin=65]}
+you can click on \pgmenu{Find} and type in the search expression
+\texttt{intro}. You will be shown a few rules ending in @{text"\<Longrightarrow> ?P \<and> ?Q"},
+among them @{thm[source]conjI}\@. You may even discover that
+the very theorem you are trying to prove is already in the
+database.  Given the goal *}
+(*<*)
+oops
+lemma "A \<longrightarrow> A"
+(*>*)
+txt{*\vspace{-\bigskipamount}
+@{subgoals[display,indent=0,margin=65]}
+the search for \texttt{intro} finds not just @{thm[source] impI}
+but also @{thm[source] imp_refl}: @{thm imp_refl}.
+
+As before, search criteria can be combined freely: for example,
+\begin{ttbox}
+"_ \at\ _"  intro
+\end{ttbox}
+searches for all introduction rules that match the current goal and
+mention the @{text"@"} function.
+
+Searching for elimination and destruction rules via \texttt{elim} and
+\texttt{dest} is analogous to \texttt{intro} but takes the assumptions
+into account, too.
+*}
+(*<*)
+oops
+end
+(*>*)