doc-src/IsarImplementation/implementation.tex
author wenzelm
Thu Aug 31 22:55:49 2006 +0200 (2006-08-31 ago)
changeset 20451 27ea2ba48fa3
parent 20064 92aad017b847
child 20472 e993073eda4c
permissions -rw-r--r--
misc cleanup;
     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 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   functions.  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 \vspace*{2.5cm}
    37 \begin{quote}
    38   
    39   {\small\em Isabelle was not designed; it evolved.  Not everyone
    40     likes this idea.  Specification experts rightly abhor
    41     trial-and-error programming.  They suggest that no one should
    42     write a program without first writing a complete formal
    43     specification. But university departments are not software houses.
    44     Programs like Isabelle are not products: when they have served
    45     their purpose, they are discarded.}
    46   
    47   Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
    48 
    49   \vspace*{1cm}
    50   
    51   {\small\em As I did 20 years ago, I still fervently believe that the
    52     only way to make software secure, reliable, and fast is to make it
    53     small.  Fight features.}
    54   
    55   Andrew S. Tanenbaum
    56 
    57 \end{quote}
    58 
    59 \thispagestyle{empty}\clearpage
    60 
    61 \pagenumbering{roman} \tableofcontents \clearfirst
    62 
    63 \input{intro.tex}
    64 \input{Thy/document/prelim.tex}
    65 \input{Thy/document/logic.tex}
    66 \input{Thy/document/tactic.tex}
    67 \input{Thy/document/proof.tex}
    68 \input{Thy/document/locale.tex}
    69 \input{Thy/document/integration.tex}
    70 
    71 \appendix
    72 \input{Thy/document/ML.tex}
    73 
    74 \begingroup
    75 \tocentry{\bibname}
    76 \bibliographystyle{plain} \small\raggedright\frenchspacing
    77 \bibliography{../manual}
    78 \endgroup
    79 
    80 \tocentry{\glossaryname}
    81 \printglossary
    82 
    83 \tocentry{\indexname}
    84 \printindex
    85 
    86 \end{document}
    87 
    88 
    89 %%% Local Variables: 
    90 %%% mode: latex
    91 %%% TeX-master: t
    92 %%% End: