added find2
authornipkow
Wed, 22 Jun 2005 19:44:12 +0200
changeset 16546 77e7fd18b785
parent 16545 916aa587dfbd
child 16547 09f7a953d2d6
added find2
doc-src/TutorialI/Rules/ROOT.ML
doc-src/TutorialI/Rules/rules.tex
--- 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
--- 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}