# HG changeset patch
# User sultana
# Date 1335272798 -3600
# Node ID 39c5a1a80accc0d88bec9946a9ad283a5a83ebc7
# Parent  15f4309bb9eb0f97d1b22d69476518d4ed84ed3a# Parent  027c7f8cef229949f64c339b3055db3f1d59dc40
merged

diff -r 15f4309bb9eb -r 39c5a1a80acc doc-src/ProgProve/Thys/Logic.thy
--- a/doc-src/ProgProve/Thys/Logic.thy	Tue Apr 24 13:59:29 2012 +0100
+++ b/doc-src/ProgProve/Thys/Logic.thy	Tue Apr 24 14:06:38 2012 +0100
@@ -244,6 +244,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} @{text"simp: \<dots> intro: \<dots>"}
+\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
@@ -410,11 +423,19 @@
 text{* In this particular example we could have backchained with
 @{thm[source] Suc_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}
 
diff -r 15f4309bb9eb -r 39c5a1a80acc doc-src/ProgProve/Thys/document/Logic.tex
--- a/doc-src/ProgProve/Thys/document/Logic.tex	Tue Apr 24 13:59:29 2012 +0100
+++ b/doc-src/ProgProve/Thys/document/Logic.tex	Tue Apr 24 14:06:38 2012 +0100
@@ -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}