--- a/src/Doc/IsarImplementation/document/root.tex Sat Apr 05 17:52:29 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,125 +0,0 @@
-\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: