doc-src/IsarImplementation/implementation.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/implementation.tex	Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,75 @@
+
+%% $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: