%% $Id$
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{latexsym,graphicx}
\usepackage[refpage]{nomencl}
\usepackage{../iman,../extra,../isar,../proof}
\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
\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 M. M. Wenzel}}
\makeglossary
\makeindex
\begin{document}
\maketitle
\begin{abstract}
We describe the key concepts underlying the Isabelle/Isar
implementation, including ML references for the most important
elements. The aim is to give some insight into the overall system
architecture, and provide clues on implementing user extensions.
\end{abstract}
\pagenumbering{roman} \tableofcontents \clearfirst
\input{intro.tex}
\input{Thy/document/prelim.tex}
\input{Thy/document/logic.tex}
\input{Thy/document/tactic.tex}
\input{Thy/document/proof.tex}
\input{Thy/document/locale.tex}
\input{Thy/document/integration.tex}
% 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.
%
% L.C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
% 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
\appendix
\input{Thy/document/ML.tex}
\begingroup
\tocentry{\bibname}
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{../manual}
\endgroup
\tocentry{\glossaryname}
\printglossary
\tocentry{\indexname}
\printindex
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: