1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarImplementation/implementation.tex	Mon Jan 02 20:16:52 2006 +0100
     1.3 @@ -0,0 +1,75 @@
     1.4 +
     1.5 +%% $Id$
     1.6 +
     1.7 +\documentclass[12pt,a4paper,fleqn]{report}
     1.8 +\usepackage{latexsym,graphicx}
     1.9 +\usepackage[refpage]{nomencl}
    1.10 +\usepackage{../iman,../extra,../isar,../proof}
    1.11 +\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
    1.12 +\usepackage{style}
    1.13 +\usepackage{../pdfsetup}
    1.14 +
    1.15 +
    1.16 +\hyphenation{Isabelle}
    1.17 +\hyphenation{Isar}
    1.18 +
    1.19 +\isadroptag{theory}
    1.20 +\title{\includegraphics[scale=0.5]{isabelle_isar}
    1.21 +  \\[4ex] The Isabelle/Isar Implementation}
    1.22 +\author{\emph{Makarius M. M. Wenzel}}
    1.23 +
    1.24 +\makeglossary
    1.25 +\makeindex
    1.26 +
    1.27 +
    1.28 +\begin{document}
    1.29 +
    1.30 +\maketitle 
    1.31 +
    1.32 +\begin{abstract}
    1.33 +  We describe the key concepts underlying the Isabelle/Isar
    1.34 +  implementation, including ML references for the most important
    1.35 +  elements.  The aim is to give some insight into the overall system
    1.36 +  architecture, and provide clues on implementing user extensions.
    1.37 +\end{abstract}
    1.38 +
    1.39 +\pagenumbering{roman} \tableofcontents \clearfirst
    1.40 +
    1.41 +\input{intro.tex}
    1.42 +\input{Thy/document/prelim.tex}
    1.43 +\input{Thy/document/logic.tex}
    1.44 +\input{Thy/document/tactic.tex}
    1.45 +\input{Thy/document/proof.tex}
    1.46 +\input{Thy/document/locale.tex}
    1.47 +\input{Thy/document/integration.tex}
    1.48 +
    1.49 +% Isabelle was not designed; it evolved.
    1.50 +% Not everyone likes this idea. Specification experts rightly abhor trial-and-error programming.
    1.51 +% They suggest that no one should write a program without First writing a complete
    1.52 +% formal specification. But university departments are not software houses. Programs like
    1.53 +% Isabelle are not products: when they have served their purpose, they are discarded.
    1.54 +%
    1.55 +% L.C. Paulson, Isabelle: The Next 700 Theorem Provers
    1.56 +
    1.57 +\appendix
    1.58 +\input{Thy/document/ML.tex}
    1.59 +
    1.60 +\begingroup
    1.61 +\tocentry{\bibname}
    1.62 +\bibliographystyle{plain} \small\raggedright\frenchspacing
    1.63 +\bibliography{../manual}
    1.64 +\endgroup
    1.65 +
    1.66 +\tocentry{\glossaryname}
    1.67 +\printglossary
    1.68 +
    1.69 +\tocentry{\indexname}
    1.70 +\printindex
    1.71 +
    1.72 +\end{document}
    1.73 +
    1.74 +
    1.75 +%%% Local Variables: 
    1.76 +%%% mode: latex
    1.77 +%%% TeX-master: t
    1.78 +%%% End: