doc-src/IsarImplementation/implementation.tex
author blanchet
Wed Mar 04 11:05:29 2009 +0100 (2009-03-04 ago)
changeset 30242 aea5d7fa7ef5
parent 30240 5b25fee0362c
parent 30124 b956bf0dc87c
child 35031 2ddc7edce107
permissions -rw-r--r--
Merge.
     1 \documentclass[12pt,a4paper,fleqn]{report}
     2 \usepackage{latexsym,graphicx}
     3 \usepackage[refpage]{nomencl}
     4 \usepackage{../iman,../extra,../isar,../proof}
     5 \usepackage[nohyphen,strings]{../underscore}
     6 \usepackage{../isabelle,../isabellesym}
     7 \usepackage{style}
     8 \usepackage{../pdfsetup}
     9 
    10 
    11 \hyphenation{Isabelle}
    12 \hyphenation{Isar}
    13 
    14 \isadroptag{theory}
    15 \title{\includegraphics[scale=0.5]{isabelle_isar}
    16   \\[4ex] The Isabelle/Isar Implementation}
    17 \author{\emph{Makarius Wenzel}  \\[3ex]
    18   With Contributions by
    19   Florian Haftmann
    20   and Larry Paulson
    21 }
    22 
    23 \makeindex
    24 
    25 
    26 \begin{document}
    27 
    28 \maketitle 
    29 
    30 \begin{abstract}
    31   We describe the key concepts underlying the Isabelle/Isar
    32   implementation, including ML references for the most important
    33   functions.  The aim is to give some insight into the overall system
    34   architecture, and provide clues on implementing applications within
    35   this framework.
    36 \end{abstract}
    37 
    38 \vspace*{2.5cm}
    39 \begin{quote}
    40   
    41   {\small\em Isabelle was not designed; it evolved.  Not everyone
    42     likes this idea.  Specification experts rightly abhor
    43     trial-and-error programming.  They suggest that no one should
    44     write a program without first writing a complete formal
    45     specification. But university departments are not software houses.
    46     Programs like Isabelle are not products: when they have served
    47     their purpose, they are discarded.}
    48   
    49   Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
    50 
    51   \vspace*{1cm}
    52   
    53   {\small\em As I did 20 years ago, I still fervently believe that the
    54     only way to make software secure, reliable, and fast is to make it
    55     small.  Fight features.}
    56   
    57   Andrew S. Tanenbaum
    58 
    59 \end{quote}
    60 
    61 \thispagestyle{empty}\clearpage
    62 
    63 \pagenumbering{roman}
    64 \tableofcontents
    65 \listoffigures
    66 \clearfirst
    67 
    68 \input{Thy/document/Prelim.tex}
    69 \input{Thy/document/Logic.tex}
    70 \input{Thy/document/Tactic.tex}
    71 \input{Thy/document/Proof.tex}
    72 \input{Thy/document/Syntax.tex}
    73 \input{Thy/document/Isar.tex}
    74 \input{Thy/document/Local_Theory.tex}
    75 \input{Thy/document/Integration.tex}
    76 
    77 \appendix
    78 \input{Thy/document/ML.tex}
    79 
    80 \begingroup
    81 \tocentry{\bibname}
    82 \bibliographystyle{abbrv} \small\raggedright\frenchspacing
    83 \bibliography{../manual}
    84 \endgroup
    85 
    86 \tocentry{\indexname}
    87 \printindex
    88 
    89 \end{document}
    90 
    91 
    92 %%% Local Variables: 
    93 %%% mode: latex
    94 %%% TeX-master: t
    95 %%% End: