diff -r b729345319f0 -r 978a3c2ed7ce CookBook/Intro.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Intro.thy	Fri Sep 05 09:47:51 2008 +0200
@@ -0,0 +1,58 @@
+theory Intro
+imports Main
+
+begin
+
+chapter {* Introduction *}
+
+text {*
+  The purpose of this document is to guide the reader through the
+  first steps in Isabelle programming, and to provide recipes for
+  solving common problems. 
+*}
+
+section {* Intended Audience and Prior Knowledge *}
+
+text {* 
+  This cookbook targets an audience who already knows how to use the Isabelle
+  system to write theories and proofs, but without using ML.
+  You should also be familiar with the \emph{Standard ML} programming
+  language, which is  used for Isabelle programming. If you are unfamiliar with any of
+  these two subjects, you should first work through the Isabelle/HOL
+  tutorial \cite{isa-tutorial} and Paulson's book on Standard ML
+  \cite{paulson-ml2}.
+
+*}
+
+section {* Primary Documentation *}
+
+text {*
+  
+
+  \begin{description}
+  \item[The Implementation Manual \cite{isa-imp}] describes Isabelle
+  from a programmer's perspective, documenting both the underlying
+  concepts and the concrete interfaces. 
+
+  \item[The Isabelle Reference Manual \cite{isabelle-ref}] is an older document that used
+  to be the main reference, when all reasoning happened on the ML
+  level. Many parts of it are outdated now, but some parts, mainly the
+  chapters on tactics, are still useful.
+
+  \item[The code] is of course the ultimate reference for how
+  things really work. Therefore you should not hesitate to look at the
+  way things are actually implemented. More importantly, it is often
+  good to look at code that does similar things as you want to do, to
+  learn from other people's code.
+  \end{description}
+
+  Since Isabelle is not a finished product, these manuals, just like
+  the implementation itself, are always under construction. This can
+  be dificult and frustrating at times, when interfaces are changing
+  frequently. But it is a reality that progress means changing
+  things (FIXME: need some short and convincing comment that this
+  is a strategy, not a problem that should be solved).
+*}
+
+
+end
\ No newline at end of file