--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/IsarImplementation/document/root.tex Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,110 @@
+\documentclass[12pt,a4paper,fleqn]{report}
+\usepackage{latexsym,graphicx}
+\usepackage[refpage]{nomencl}
+\usepackage{iman,extra,isar,proof}
+\usepackage[nohyphen,strings]{underscore}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{railsetup}
+\usepackage{ttbox}
+\usepackage{style}
+\usepackage{pdfsetup}
+
+
+\hyphenation{Isabelle}
+\hyphenation{Isar}
+
+\isadroptag{theory}
+\title{\includegraphics[scale=0.5]{isabelle_isar}
+ \\[4ex] The Isabelle/Isar Implementation}
+\author{\emph{Makarius Wenzel} \\[3ex]
+ With Contributions by
+ Florian Haftmann
+ and Larry Paulson
+}
+
+\makeindex
+
+
+\begin{document}
+
+\maketitle
+
+\begin{abstract}
+ We describe the key concepts underlying the Isabelle/Isar
+ implementation, including ML references for the most important
+ functions. The aim is to give some insight into the overall system
+ architecture, and provide clues on implementing applications within
+ this framework.
+\end{abstract}
+
+\vspace*{2.5cm}
+\begin{quote}
+
+ {\small\em Isabelle was not designed; it evolved. Not everyone
+ likes this idea. Specification experts rightly abhor
+ trial-and-error programming. They suggest that no one should
+ write a program without first writing a complete formal
+ specification. But university departments are not software houses.
+ Programs like Isabelle are not products: when they have served
+ their purpose, they are discarded.}
+
+ Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
+
+ \vspace*{1cm}
+
+ {\small\em As I did 20 years ago, I still fervently believe that the
+ only way to make software secure, reliable, and fast is to make it
+ small. Fight features.}
+
+ Andrew S. Tanenbaum
+
+ \vspace*{1cm}
+
+ {\small\em One thing that UNIX does not need is more features. It is
+ successful in part because it has a small number of good ideas
+ that work well together. Merely adding features does not make it
+ easier for users to do things --- it just makes the manual
+ thicker. The right solution in the right place is always more
+ effective than haphazard hacking.}
+
+ Rob Pike and Brian W. Kernighan
+
+\end{quote}
+
+\thispagestyle{empty}\clearpage
+
+\pagenumbering{roman}
+\tableofcontents
+\listoffigures
+\clearfirst
+
+\setcounter{chapter}{-1}
+
+\input{ML.tex}
+\input{Prelim.tex}
+\input{Logic.tex}
+\input{Syntax.tex}
+\input{Tactic.tex}
+\input{Eq.tex}
+\input{Proof.tex}
+\input{Isar.tex}
+\input{Local_Theory.tex}
+\input{Integration.tex}
+
+\begingroup
+\tocentry{\bibname}
+\bibliographystyle{abbrv} \small\raggedright\frenchspacing
+\bibliography{manual}
+\endgroup
+
+\tocentry{\indexname}
+\printindex
+
+\end{document}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: