doc-src/IsarImplementation/implementation.tex

added type global_theory -- theory or local_theory;
added begin/exit_local_theory;
removed theory_context;
renamed body_context_node to presentation_context;
removed copy (checkpoint twice instead -- avoids unrelated theories);

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

%FIXME
%\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 applications within
  this framework.
\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
\listoffigures
\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

%FIXME
%\tocentry{\glossaryname}
%\printglossary

\tocentry{\indexname}
\printindex

\end{document}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: