--- a/doc-src/TutorialI/Rules/document/find2.tex Thu Jul 26 16:08:16 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,101 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{find{\isadigit{2}}}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\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 \begin{isabelle}%
-\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B%
-\end{isabelle}
-you can click on \pgmenu{Find} and type in the search expression
-\texttt{intro}. You will be shown a few rules ending in \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q},
-among them \isa{conjI}\@. You may even discover that
-the very theorem you are trying to prove is already in the
-database. Given the goal%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\vspace{-\bigskipamount}
-\begin{isabelle}%
-\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A%
-\end{isabelle}
-the search for \texttt{intro} finds not just \isa{impI}
-but also \isa{imp{\isaliteral{5F}{\isacharunderscore}}refl}: \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P}.
-
-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 \isa{{\isaliteral{40}{\isacharat}}} 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.%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: