doc-src/IsarImplementation/implementation.tex

"The Isabelle/Isar Implementation" manual;

%% $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

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