split the document into smaller pieces;
made it standalone by copying antiquote_setup.ML into the repository
added cover page
theory Introimports Mainbeginchapter {* 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