1\documentclass[12pt,a4paper,fleqn]{report}
2\usepackage{lmodern}
3\usepackage[T1]{fontenc}
4\usepackage{latexsym,graphicx}
5\usepackage[refpage]{nomencl}
6\usepackage{iman,extra,isar,proof}
7\usepackage[nohyphen,strings]{underscore}
8\usepackage{isabelle}
9\usepackage{isabellesym}
10\usepackage{railsetup}
11\usepackage{supertabular}
12\usepackage{style}
13\usepackage{pdfsetup}
14
15
16\hyphenation{Isabelle}
17\hyphenation{Isar}
18
19\isadroptag{theory}
20\title{\includegraphics[scale=0.5]{isabelle_isar}
21  \\[4ex] The Isabelle/Isar Implementation}
22\author{\emph{Makarius Wenzel}  \\[3ex]
23  With Contributions by
24  Stefan Berghofer, \\
25  Florian Haftmann
26  and Larry Paulson
27}
28
29\makeindex
30
31
32\begin{document}
33
34\maketitle
35
36\begin{abstract}
37  We describe the key concepts underlying the Isabelle/Isar
38  implementation, including ML references for the most important
39  functions.  The aim is to give some insight into the overall system
40  architecture, and provide clues on implementing applications within
41  this framework.
42\end{abstract}
43
44\vspace*{2.5cm}
45\begin{quote}
46
47  {\small\em Isabelle was not designed; it evolved.  Not everyone
48    likes this idea.  Specification experts rightly abhor
49    trial-and-error programming.  They suggest that no one should
50    write a program without first writing a complete formal
51    specification. But university departments are not software houses.
52    Programs like Isabelle are not products: when they have served
53    their purpose, they are discarded.}
54
55  Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
56
57  \vspace*{1cm}
58
59  {\small\em As I did 20 years ago, I still fervently believe that the
60    only way to make software secure, reliable, and fast is to make it
61    small.  Fight features.}
62
63  Andrew S. Tanenbaum
64
65  \vspace*{1cm}
66
67  {\small\em One thing that UNIX does not need is more features. It is
68    successful in part because it has a small number of good ideas
69    that work well together. Merely adding features does not make it
70    easier for users to do things --- it just makes the manual
71    thicker. The right solution in the right place is always more
72    effective than haphazard hacking.}
73
74  Rob Pike and Brian W. Kernighan
75
76  \vspace*{1cm}
77
78  {\small\em If you look at software today, through the lens of the
79    history of engineering, it's certainly engineering of a sort--but
80    it's the kind of engineering that people without the concept of
81    the arch did. Most software today is very much like an Egyptian
82    pyramid with millions of bricks piled on top of each other, with
83    no structural integrity, but just done by brute force and
84    thousands of slaves.}
85
86  Alan Kay
87
88\end{quote}
89
90\thispagestyle{empty}\clearpage
91
92\pagenumbering{roman}
93\tableofcontents
94\listoffigures
95\clearfirst
96
97\setcounter{chapter}{-1}
98
99\input{ML.tex}
100\input{Prelim.tex}
101\input{Logic.tex}
102\input{Syntax.tex}
103\input{Tactic.tex}
104\input{Eq.tex}
105\input{Proof.tex}
106\input{Isar.tex}
107\input{Local_Theory.tex}
108\input{Integration.tex}
109
110\begingroup
111\tocentry{\bibname}
112\bibliographystyle{abbrv} \small\raggedright\frenchspacing
113\bibliography{manual}
114\endgroup
115
116\tocentry{\indexname}
117\printindex
118
119\end{document}
120
121
122%%% Local Variables:
123%%% mode: latex
124%%% TeX-master: t
125%%% End:
126