author sultana Tue, 24 Apr 2012 14:06:38 +0100 changeset 47731 39c5a1a80acc parent 47730 15f4309bb9eb (current diff) parent 47727 027c7f8cef22 (diff) child 47732 503efdb07566
merged
--- 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}

--- 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}