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: