doc-src/IsarImplementation/implementation.tex
author haftmann
Fri Dec 29 12:11:04 2006 +0100 (2006-12-29)
changeset 21927 9677abe5d374
parent 20514 5ede702cd2ca
child 22868 c82dd66560ac
permissions -rw-r--r--
added handling for explicit classrel witnesses
     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 %FIXME
    22 %\makeglossary
    23 
    24 \makeindex
    25 
    26 
    27 \begin{document}
    28 
    29 \maketitle 
    30 
    31 \begin{abstract}
    32   We describe the key concepts underlying the Isabelle/Isar
    33   implementation, including ML references for the most important
    34   functions.  The aim is to give some insight into the overall system
    35   architecture, and provide clues on implementing applications within
    36   this framework.
    37 \end{abstract}
    38 
    39 \vspace*{2.5cm}
    40 \begin{quote}
    41   
    42   {\small\em Isabelle was not designed; it evolved.  Not everyone
    43     likes this idea.  Specification experts rightly abhor
    44     trial-and-error programming.  They suggest that no one should
    45     write a program without first writing a complete formal
    46     specification. But university departments are not software houses.
    47     Programs like Isabelle are not products: when they have served
    48     their purpose, they are discarded.}
    49   
    50   Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
    51 
    52   \vspace*{1cm}
    53   
    54   {\small\em As I did 20 years ago, I still fervently believe that the
    55     only way to make software secure, reliable, and fast is to make it
    56     small.  Fight features.}
    57   
    58   Andrew S. Tanenbaum
    59 
    60 \end{quote}
    61 
    62 \thispagestyle{empty}\clearpage
    63 
    64 \pagenumbering{roman}
    65 \tableofcontents
    66 \listoffigures
    67 \clearfirst
    68 
    69 \input{intro.tex}
    70 \input{Thy/document/prelim.tex}
    71 \input{Thy/document/logic.tex}
    72 \input{Thy/document/tactic.tex}
    73 \input{Thy/document/proof.tex}
    74 \input{Thy/document/isar.tex}
    75 \input{Thy/document/locale.tex}
    76 \input{Thy/document/integration.tex}
    77 
    78 \appendix
    79 \input{Thy/document/ML.tex}
    80 
    81 \begingroup
    82 \tocentry{\bibname}
    83 \bibliographystyle{plain} \small\raggedright\frenchspacing
    84 \bibliography{../manual}
    85 \endgroup
    86 
    87 %FIXME
    88 %\tocentry{\glossaryname}
    89 %\printglossary
    90 
    91 \tocentry{\indexname}
    92 \printindex
    93 
    94 \end{document}
    95 
    96 
    97 %%% Local Variables: 
    98 %%% mode: latex
    99 %%% TeX-master: t
   100 %%% End: