wneuper/isa: doc-src/IsarImplementation/implementation.tex@be234c04401a

     2 %% $Id$

     4 \documentclass[12pt,a4paper,fleqn]{report}

     5 \usepackage{latexsym,graphicx}

     6 \usepackage[refpage]{nomencl}

     7 \usepackage{../iman,../extra,../isar,../proof}

     8 \usepackage[nohyphen,strings]{../underscore}

     9 \usepackage{../isabelle,../isabellesym}

    10 \usepackage{style}

    11 \usepackage{../pdfsetup}

    14 \hyphenation{Isabelle}

    15 \hyphenation{Isar}

    17 \isadroptag{theory}

    18 \title{\includegraphics[scale=0.5]{isabelle_isar}

    19   \\[4ex] The Isabelle/Isar Implementation}

    20 \author{\emph{Makarius Wenzel}  \\[3ex]

    21   With Contributions by

    22   Florian Haftmann

    23   and Larry Paulson

    24 }

    26 %FIXME

    27 %\makeglossary

    29 \makeindex

    32 \begin{document}

    34 \maketitle

    36 \begin{abstract}

    37   We describe the key concepts underlying the Isabelle/Isar

    38   implementation, including ML references for the most important

    39   functions.  The aim is to give some insight into the overall system

    40   architecture, and provide clues on implementing applications within

    41   this framework.

    42 \end{abstract}

    44 \vspace*{2.5cm}

    45 \begin{quote}

    47   {\small\em Isabelle was not designed; it evolved.  Not everyone

    48     likes this idea.  Specification experts rightly abhor

    49     trial-and-error programming.  They suggest that no one should

    50     write a program without first writing a complete formal

    51     specification. But university departments are not software houses.

    52     Programs like Isabelle are not products: when they have served

    53     their purpose, they are discarded.}

    55   Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''

    57   \vspace*{1cm}

    59   {\small\em As I did 20 years ago, I still fervently believe that the

    60     only way to make software secure, reliable, and fast is to make it

    61     small.  Fight features.}

    63   Andrew S. Tanenbaum

    65 \end{quote}

    67 \thispagestyle{empty}\clearpage

    69 \pagenumbering{roman}

    70 \tableofcontents

    71 \listoffigures

    72 \clearfirst

    74 %\input{intro.tex}

    75 \input{Thy/document/prelim.tex}

    76 \input{Thy/document/logic.tex}

    77 \input{Thy/document/tactic.tex}

    78 \input{Thy/document/proof.tex}

    79 \input{Thy/document/isar.tex}

    80 \input{Thy/document/locale.tex}

    81 \input{Thy/document/integration.tex}

    83 \appendix

    84 \input{Thy/document/ML.tex}

    86 \begingroup

    87 \tocentry{\bibname}

    88 \bibliographystyle{plain} \small\raggedright\frenchspacing

    89 \bibliography{../manual}

    90 \endgroup

    92 %FIXME

    93 %\tocentry{\glossaryname}

    94 %\printglossary

    96 \tocentry{\indexname}

    97 \printindex

    99 \end{document}

   102 %%% Local Variables:

   103 %%% mode: latex

   104 %%% TeX-master: t

   105 %%% End:

author	wenzelm
	Thu, 13 Nov 2008 22:03:26 +0100
changeset 28780	be234c04401a
parent 26906	6e8152678e06
child 30081	d66b34e46bdf
child 30240	5b25fee0362c
permissions	-rw-r--r--