--- a/CookBook/Intro.thy Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,166 +0,0 @@
-theory Intro
-imports Base
-
-begin
-
-
-chapter {* Introduction *}
-
-text {*
- If your next project requires you to program on the ML-level of Isabelle,
- then this tutorial is for you. It will guide you through the first steps of
- Isabelle programming, and also explain tricks of the trade. The best way to
- get to know the ML-level of Isabelle is by experimenting with the many code
- examples included in the tutorial. The code is as far as possible checked
- against recent versions of Isabelle. If something does not work, then
- please let us know. If you have comments, criticism or like to add to the
- tutorial, please feel free---you are most welcome! The tutorial is meant to be
- gentle and comprehensive. To achieve this we need your feedback.
-*}
-
-section {* Intended Audience and Prior Knowledge *}
-
-text {*
- This tutorial targets readers who already know how to use Isabelle for
- writing theories and proofs. We also assume that readers are familiar with
- the functional programming language ML, the language in which most of
- Isabelle is implemented. If you are unfamiliar with either of these two
- subjects, you should first work through the Isabelle/HOL tutorial
- \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.
-
-*}
-
-section {* Existing Documentation *}
-
-text {*
-
- The following documentation about Isabelle programming already exists (and is
- part of the distribution of Isabelle):
-
- \begin{description}
- \item[The Isabelle/Isar Implementation Manual] describes Isabelle
- from a high-level perspective, documenting both the underlying
- concepts and some of the interfaces.
-
- \item[The Isabelle Reference Manual] is an older document that used
- to be the main reference of Isabelle at a time when all proof scripts
- were written on the ML-level. Many parts of this manual are outdated
- now, but some parts, particularly the chapters on tactics, are still
- useful.
-
- \item[The Isar Reference Manual] provides specification material (like grammars,
- examples and so on) about Isar and its implementation. It is currently in
- the process of being updated.
- \end{description}
-
- Then of course there is:
-
- \begin{description}
- \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 and
- to learn from that code. The UNIX command @{text "grep -R"} is
- often your best friend while programming with Isabelle.
- \end{description}
-
-*}
-
-section {* Typographic Conventions *}
-
-text {*
-
- All ML-code in this tutorial is typeset in shaded boxes, like the following
- ML-expression:
-
- \begin{isabelle}
- \begin{graybox}
- \isacommand{ML}~@{text "\<verbopen>"}\isanewline
- \hspace{5mm}@{ML "3 + 4"}\isanewline
- @{text "\<verbclose>"}
- \end{graybox}
- \end{isabelle}
-
- These boxes corresponds to how code can be processed inside the interactive
- environment of Isabelle. It is therefore easy to experiment with what is
- displayed. However, for better readability we will drop the enclosing
- \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write:
-
-
- @{ML [display,gray] "3 + 4"}
-
- Whenever appropriate we also show the response the code
- generates when evaluated. This response is prefixed with a
- @{text [quotes] ">"}, like:
-
- @{ML_response [display,gray] "3 + 4" "7"}
-
- The user-level commands of Isabelle (i.e.~the non-ML code) are written
- in bold, for example \isacommand{lemma}, \isacommand{apply},
- \isacommand{foobar} and so on. We use @{text "$ \<dots>"} to indicate that a
- command needs to be run in a Unix-shell, for example:
-
- @{text [display] "$ grep -R ThyOutput *"}
-
- Pointers to further information and Isabelle files are typeset in
- italic and highlighted as follows:
-
- \begin{readmore}
- Further information or pointers to files.
- \end{readmore}
-
- The pointers to Isabelle files are hyperlinked to the tip of the Mercurial
- repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/}
- {http://isabelle.in.tum.de/repos/isabelle/}.
-
- A few exercises are scattered around the text. Their solutions are given
- in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
- to solve the exercises on your own, and then look at the solutions.
-
-*}
-
-section {* Acknowledgements *}
-
-text {*
- Financial support for this tutorial was provided by the German
- Research Council (DFG) under grant number URB 165/5-1. The following
- people contributed to the text:
-
- \begin{itemize}
- \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
- \simpleinductive-package and the code for the @{text
- "chunk"}-antiquotation. He also wrote the first version of the chapter
- describing the package and has been helpful \emph{beyond measure} with
- answering questions about Isabelle.
-
- \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout},
- \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.
- He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}.
-
- \item {\bf Jeremy Dawson} wrote the first version of the chapter
- about parsing.
-
- \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
-
- \item {\bf Alexander Krauss} wrote the first version of the ``first-steps''
- chapter and also contributed the material on @{text NamedThmsFun}.
- \end{itemize}
-
- Please let me know of any omissions. Responsibility for any remaining
- errors lies with me.\bigskip
-
- {\Large\bf
- This document is still in the process of being written! All of the
- text is still under constructions. Sections and
- chapters that are under \underline{heavy} construction are marked
- with TBD.}
-
-
- \vfill
- This document was compiled with:\\
- \input{version}
-*}
-
-
-
-end
\ No newline at end of file