doc-src/IsarImplementation/implementation.tex
changeset 18537 2681f9e34390
child 18554 bff7a1466fe4
equal deleted inserted replaced
18536:ab3f32f86847 18537:2681f9e34390
       
     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: