--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Intro/document/root.tex Mon Aug 27 20:50:10 2012 +0200
@@ -0,0 +1,154 @@
+\documentclass[12pt,a4paper]{article}
+\usepackage{graphicx,iman,extra,ttbox,proof,pdfsetup}
+
+%% run bibtex intro to prepare bibliography
+%% run ../sedindex intro to prepare index file
+%prth *(\(.*\)); \1;
+%{\\out \(.*\)} {\\out val it = "\1" : thm}
+
+\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Introduction to Isabelle}
+\author{{\em Lawrence C. Paulson}\\
+ Computer Laboratory \\ University of Cambridge \\
+ \texttt{lcp@cl.cam.ac.uk}\\[3ex]
+ With Contributions by Tobias Nipkow and Markus Wenzel
+}
+\makeindex
+
+\underscoreoff
+
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+\sloppy
+\binperiod %%%treat . like a binary operator
+
+\newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification
+\newcommand{\nand}{\mathbin{\lnot\&}}
+\newcommand{\xor}{\mathbin{\#}}
+
+\pagenumbering{roman}
+\begin{document}
+\pagestyle{empty}
+\begin{titlepage}
+\maketitle
+\emph{Note}: this document is part of the earlier Isabelle documentation,
+which is largely superseded by the Isabelle/HOL
+\emph{Tutorial}~\cite{isa-tutorial}. It describes the old-style theory
+syntax and shows how to conduct proofs using the
+ML top level. This style of interaction is largely obsolete:
+most Isabelle proofs are now written using the Isar
+language and the Proof General interface. However, this paper contains valuable
+information that is not available elsewhere. Its examples are based
+on first-order logic rather than higher-order logic.
+
+\thispagestyle{empty}
+\vfill
+{\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
+\end{titlepage}
+
+\pagestyle{headings}
+\part*{Preface}
+\index{Isabelle!overview} \index{Isabelle!object-logics supported}
+Isabelle~\cite{paulson-natural,paulson-found,paulson700} is a generic theorem
+prover. It has been instantiated to support reasoning in several
+object-logics:
+\begin{itemize}
+\item first-order logic, constructive and classical versions
+\item higher-order logic, similar to that of Gordon's {\sc
+hol}~\cite{mgordon-hol}
+\item Zermelo-Fraenkel set theory~\cite{suppes72}
+\item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
+\item the classical first-order sequent calculus, {\sc lk}
+\item the modal logics $T$, $S4$, and $S43$
+\item the Logic for Computable Functions~\cite{paulson87}
+\end{itemize}
+A logic's syntax and inference rules are specified declaratively; this
+allows single-step proof construction. Isabelle provides control
+structures for expressing search procedures. Isabelle also provides
+several generic tools, such as simplifiers and classical theorem provers,
+which can be applied to object-logics.
+
+Isabelle is a large system, but beginners can get by with a small
+repertoire of commands and a basic knowledge of how Isabelle works.
+The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some
+knowledge of Standard~\ML{}, because Isabelle is written in \ML{};
+\index{ML}
+if you are prepared to writing \ML{}
+code, you can get Isabelle to do almost anything. My book
+on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle,
+including a simple theorem prover. Users must be familiar with logic as
+used in computer science; there are many good
+texts~\cite{galton90,reeves90}.
+
+\index{LCF}
+{\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an
+ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows
+ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
+abstract type; tactics and tacticals support backward proof. But {\sc lcf}
+represents object-level rules by functions, while Isabelle represents them
+by terms. You may find my other writings~\cite{paulson87,paulson-handbook}
+helpful in understanding the relationship between {\sc lcf} and Isabelle.
+
+\index{Isabelle!release history} Isabelle was first distributed in 1986.
+The 1987 version introduced a higher-order meta-logic with an improved
+treatment of quantifiers. The 1988 version added limited polymorphism and
+support for natural deduction. The 1989 version included a parser and
+pretty printer generator. The 1992 version introduced type classes, to
+support many-sorted and higher-order logics. The 1994 version introduced
+greater support for theories. The most important recent change is the
+introduction of the Isar proof language, thanks to Markus Wenzel.
+Isabelle is still under
+development and will continue to change.
+
+\subsubsection*{Overview}
+This manual consists of three parts. Part~I discusses the Isabelle's
+foundations. Part~II, presents simple on-line sessions, starting with
+forward proof. It also covers basic tactics and tacticals, and some
+commands for invoking them. Part~III contains further examples for users
+with a bit of experience. It explains how to derive rules define theories,
+and concludes with an extended example: a Prolog interpreter.
+
+Isabelle's Reference Manual and Object-Logics manual contain more details.
+They assume familiarity with the concepts presented here.
+
+
+\subsubsection*{Acknowledgements}
+Tobias Nipkow contributed most of the section on defining theories.
+Stefan Berghofer, Sara Kalvala and Viktor Kuncak suggested improvements.
+
+Tobias Nipkow has made immense contributions to Isabelle, including the parser
+generator, type classes, and the simplifier. Carsten Clasohm and Markus
+Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also
+helped. Isabelle was developed using Dave Matthews's Standard~{\sc ml}
+compiler, Poly/{\sc ml}. Many people have contributed to Isabelle's standard
+object-logics, including Martin Coen, Philippe de Groote, Philippe No\"el.
+The research has been funded by the EPSRC (grants GR/G53279, GR/H40570,
+GR/K57381, GR/K77051, GR/M75440) and by ESPRIT (projects 3245: Logical
+Frameworks, and 6453: Types), and by the DFG Schwerpunktprogramm
+\emph{Deduktion}.
+
+\newpage
+\pagestyle{plain} \tableofcontents
+\newpage
+
+\newfont{\sanssi}{cmssi12}
+\vspace*{2.5cm}
+\begin{quote}
+\raggedleft
+{\sanssi
+You can only find truth with logic\\
+if you have already found truth without it.}\\
+\bigskip
+
+G.K. Chesterton, {\em The Man who was Orthodox}
+\end{quote}
+
+\clearfirst \pagestyle{headings}
+\include{foundations}
+\include{getting}
+\include{advanced}
+
+\bibliographystyle{plain} \small\raggedright\frenchspacing
+\bibliography{manual}
+
+\printindex
+\end{document}