# HG changeset patch
# User nipkow
# Date 1119462252 -7200
# Node ID 77e7fd18b7852ab3e9414437c4ee6d2fa88ef217
# Parent  916aa587dfbd2498b04691ee86221481b3258f4c
added find2

diff -r 916aa587dfbd -r 77e7fd18b785 doc-src/TutorialI/Rules/ROOT.ML
--- a/doc-src/TutorialI/Rules/ROOT.ML	Wed Jun 22 19:44:03 2005 +0200
+++ b/doc-src/TutorialI/Rules/ROOT.ML	Wed Jun 22 19:44:12 2005 +0200
@@ -5,3 +5,4 @@
 use_thy "Forward";
 use_thy "Tacticals";
 
+use_thy "find2";
\ No newline at end of file
diff -r 916aa587dfbd -r 77e7fd18b785 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Wed Jun 22 19:44:03 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Wed Jun 22 19:44:12 2005 +0200
@@ -1808,6 +1808,10 @@
 \end{tabular}
 \end{center}
 
+\section{Finding More Theorems}
+\label{sec:find2}
+\input{Rules/document/find2.tex}
+
 
 \section{Forward Proof: Transforming Theorems}\label{sec:forward}