doc-src/IsarImplementation/implementation.tex
 author wenzelm Fri Aug 12 22:10:49 2011 +0200 (2011-08-12) changeset 44163 32e0c150c010 parent 42632 ebec0c1a5984 child 46295 2548a85b0e02 permissions -rw-r--r--
normalized theory dependencies wrt. file_store;
     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{../../lib/texinputs/isabelle}

     7 \usepackage{../../lib/texinputs/isabellesym}

     8 \usepackage{../../lib/texinputs/railsetup}

     9 \usepackage{../ttbox}

    10 \usepackage{style}

    11 \usepackage{../pdfsetup}

    12

    13

    14 \hyphenation{Isabelle}

    15 \hyphenation{Isar}

    16

    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 }

    25

    26 \makeindex

    27

    28

    29 \begin{document}

    30

    31 \maketitle

    32

    33 \begin{abstract}

    34   We describe the key concepts underlying the Isabelle/Isar

    35   implementation, including ML references for the most important

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

    37   architecture, and provide clues on implementing applications within

    38   this framework.

    39 \end{abstract}

    40

    41 \vspace*{2.5cm}

    42 \begin{quote}

    43

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

    45     likes this idea.  Specification experts rightly abhor

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

    47     write a program without first writing a complete formal

    48     specification. But university departments are not software houses.

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

    50     their purpose, they are discarded.}

    51

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

    53

    54   \vspace*{1cm}

    55

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

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

    58     small.  Fight features.}

    59

    60   Andrew S. Tanenbaum

    61

    62   \vspace*{1cm}

    63

    64   {\small\em One thing that UNIX does not need is more features. It is

    65     successful in part because it has a small number of good ideas

    66     that work well together. Merely adding features does not make it

    67     easier for users to do things --- it just makes the manual

    68     thicker. The right solution in the right place is always more

    69     effective than haphazard hacking.}

    70

    71   Rob Pike and Brian W. Kernighan

    72

    73 \end{quote}

    74

    75 \thispagestyle{empty}\clearpage

    76

    77 \pagenumbering{roman}

    78 \tableofcontents

    79 \listoffigures

    80 \clearfirst

    81

    82 \setcounter{chapter}{-1}

    83

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

    85 \input{Thy/document/Prelim.tex}

    86 \input{Thy/document/Logic.tex}

    87 \input{Thy/document/Syntax.tex}

    88 \input{Thy/document/Tactic.tex}

    89 \input{Thy/document/Proof.tex}

    90 \input{Thy/document/Isar.tex}

    91 \input{Thy/document/Local_Theory.tex}

    92 \input{Thy/document/Integration.tex}

    93

    94 \begingroup

    95 \tocentry{\bibname}

    96 \bibliographystyle{abbrv} \small\raggedright\frenchspacing

    97 \bibliography{../manual}

    98 \endgroup

    99

   100 \tocentry{\indexname}

   101 \printindex

   102

   103 \end{document}

   104

   105

   106 %%% Local Variables:

   107 %%% mode: latex

   108 %%% TeX-master: t

   109 %%% End: