doc-src/IsarImplementation/implementation.tex
author wenzelm
Mon Jan 02 20:16:52 2006 +0100 (2006-01-02 ago)
changeset 18537 2681f9e34390
child 18554 bff7a1466fe4
permissions -rw-r--r--
"The Isabelle/Isar Implementation" manual;
     1 
     2 %% $Id$
     3 
     4 \documentclass[12pt,a4paper,fleqn]{report}
     5 \usepackage{latexsym,graphicx}
     6 \usepackage[refpage]{nomencl}
     7 \usepackage{../iman,../extra,../isar,../proof}
     8 \usepackage{Thy/document/isabelle,Thy/document/isabellesym}
     9 \usepackage{style}
    10 \usepackage{../pdfsetup}
    11 
    12 
    13 \hyphenation{Isabelle}
    14 \hyphenation{Isar}
    15 
    16 \isadroptag{theory}
    17 \title{\includegraphics[scale=0.5]{isabelle_isar}
    18   \\[4ex] The Isabelle/Isar Implementation}
    19 \author{\emph{Makarius M. M. Wenzel}}
    20 
    21 \makeglossary
    22 \makeindex
    23 
    24 
    25 \begin{document}
    26 
    27 \maketitle 
    28 
    29 \begin{abstract}
    30   We describe the key concepts underlying the Isabelle/Isar
    31   implementation, including ML references for the most important
    32   elements.  The aim is to give some insight into the overall system
    33   architecture, and provide clues on implementing user extensions.
    34 \end{abstract}
    35 
    36 \pagenumbering{roman} \tableofcontents \clearfirst
    37 
    38 \input{intro.tex}
    39 \input{Thy/document/prelim.tex}
    40 \input{Thy/document/logic.tex}
    41 \input{Thy/document/tactic.tex}
    42 \input{Thy/document/proof.tex}
    43 \input{Thy/document/locale.tex}
    44 \input{Thy/document/integration.tex}
    45 
    46 % Isabelle was not designed; it evolved.
    47 % Not everyone likes this idea. Specification experts rightly abhor trial-and-error programming.
    48 % They suggest that no one should write a program without First writing a complete
    49 % formal specification. But university departments are not software houses. Programs like
    50 % Isabelle are not products: when they have served their purpose, they are discarded.
    51 %
    52 % L.C. Paulson, Isabelle: The Next 700 Theorem Provers
    53 
    54 \appendix
    55 \input{Thy/document/ML.tex}
    56 
    57 \begingroup
    58 \tocentry{\bibname}
    59 \bibliographystyle{plain} \small\raggedright\frenchspacing
    60 \bibliography{../manual}
    61 \endgroup
    62 
    63 \tocentry{\glossaryname}
    64 \printglossary
    65 
    66 \tocentry{\indexname}
    67 \printindex
    68 
    69 \end{document}
    70 
    71 
    72 %%% Local Variables: 
    73 %%% mode: latex
    74 %%% TeX-master: t
    75 %%% End: