
%% $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 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
  functions.  The aim is to give some insight into the overall system
  architecture, and provide clues on implementing user extensions.
\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

\end{quote}

\thispagestyle{empty}\clearpage

\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/isar.tex}
\input{Thy/document/locale.tex}
\input{Thy/document/integration.tex}

\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: 
