doc-src/ProgProve/Thys/document/Logic.tex

--- a/doc-src/ProgProve/Thys/document/Logic.tex	Tue Apr 24 11:07:50 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Logic.tex	Tue Apr 24 12:36:27 2012 +0200
@@ -347,6 +347,19 @@
 but we will not enlarge on that here.
 
 
+\subsubsection{Trying them all}
+
+If you want to try all of the above automatic proof methods you simply type
+\begin{isabelle}
+\isacom{try}
+\end{isabelle}
+You can also add specific simplification and introduction rules:
+\begin{isabelle}
+\isacom{try} \isa{simp{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ intro{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}}
+\end{isabelle}
+There is also a lightweight variant \isacom{try0} that does not call
+sledgehammer.
+
 \subsection{Single step proofs}
 
 Although automation is nice, it often fails, at least initially, and you need
@@ -541,11 +554,19 @@
 In this particular example we could have backchained with
 \isa{Suc{\isaliteral{5F}{\isacharunderscore}}leD}, too, but because the premise is more complicated than the conclusion this can easily lead to nontermination.
 
+\subsubsection{Finding theorems}
+
+Command \isacom{find\_theorems} searches for specific theorems in the current
+theory. Search criteria include pattern matching on terms and on names.
+For details see the Isabelle/Isar Reference Manual~\cite{IsarRef}.
+\bigskip
+
 \begin{warn}
 To ease readability we will drop the question marks
 in front of unknowns from now on.
 \end{warn}
 
+
 \section{Inductive definitions}
 \label{sec:inductive-defs}