--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Implementation/document/root.tex Sat Apr 05 11:37:00 2014 +0200
@@ -0,0 +1,125 @@
+\documentclass[12pt,a4paper,fleqn]{report}
+\usepackage[T1]{fontenc}
+\usepackage{latexsym,graphicx}
+\usepackage[refpage]{nomencl}
+\usepackage{iman,extra,isar,proof}
+\usepackage[nohyphen,strings]{underscore}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{railsetup}
+\usepackage{ttbox}
+\usepackage{supertabular}
+\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
+ Stefan Berghofer, \\
+ 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
+
+ \vspace*{1cm}
+
+ {\small\em If you look at software today, through the lens of the
+ history of engineering, it's certainly engineering of a sort--but
+ it's the kind of engineering that people without the concept of
+ the arch did. Most software today is very much like an Egyptian
+ pyramid with millions of bricks piled on top of each other, with
+ no structural integrity, but just done by brute force and
+ thousands of slaves.}
+
+ Alan Kay
+
+\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: