doc-src/IsarImplementation/implementation.tex
author wenzelm
Tue Jan 03 13:59:55 2006 +0100 (2006-01-03 ago)
changeset 18554 bff7a1466fe4
parent 18537 2681f9e34390
child 19189 dbc19b772f5b
permissions -rw-r--r--
more stuff;
wenzelm@18537
     1
wenzelm@18537
     2
%% $Id$
wenzelm@18537
     3
wenzelm@18537
     4
\documentclass[12pt,a4paper,fleqn]{report}
wenzelm@18537
     5
\usepackage{latexsym,graphicx}
wenzelm@18537
     6
\usepackage[refpage]{nomencl}
wenzelm@18537
     7
\usepackage{../iman,../extra,../isar,../proof}
wenzelm@18537
     8
\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
wenzelm@18537
     9
\usepackage{style}
wenzelm@18537
    10
\usepackage{../pdfsetup}
wenzelm@18537
    11
wenzelm@18537
    12
wenzelm@18537
    13
\hyphenation{Isabelle}
wenzelm@18537
    14
\hyphenation{Isar}
wenzelm@18537
    15
wenzelm@18537
    16
\isadroptag{theory}
wenzelm@18537
    17
\title{\includegraphics[scale=0.5]{isabelle_isar}
wenzelm@18537
    18
  \\[4ex] The Isabelle/Isar Implementation}
wenzelm@18537
    19
\author{\emph{Makarius M. M. Wenzel}}
wenzelm@18537
    20
wenzelm@18537
    21
\makeglossary
wenzelm@18537
    22
\makeindex
wenzelm@18537
    23
wenzelm@18537
    24
wenzelm@18537
    25
\begin{document}
wenzelm@18537
    26
wenzelm@18537
    27
\maketitle 
wenzelm@18537
    28
wenzelm@18537
    29
\begin{abstract}
wenzelm@18537
    30
  We describe the key concepts underlying the Isabelle/Isar
wenzelm@18537
    31
  implementation, including ML references for the most important
wenzelm@18537
    32
  elements.  The aim is to give some insight into the overall system
wenzelm@18537
    33
  architecture, and provide clues on implementing user extensions.
wenzelm@18537
    34
\end{abstract}
wenzelm@18537
    35
wenzelm@18537
    36
\pagenumbering{roman} \tableofcontents \clearfirst
wenzelm@18537
    37
wenzelm@18537
    38
\input{intro.tex}
wenzelm@18537
    39
\input{Thy/document/prelim.tex}
wenzelm@18537
    40
\input{Thy/document/logic.tex}
wenzelm@18537
    41
\input{Thy/document/tactic.tex}
wenzelm@18537
    42
\input{Thy/document/proof.tex}
wenzelm@18537
    43
\input{Thy/document/locale.tex}
wenzelm@18537
    44
\input{Thy/document/integration.tex}
wenzelm@18537
    45
wenzelm@18537
    46
% Isabelle was not designed; it evolved.
wenzelm@18537
    47
% Not everyone likes this idea. Specification experts rightly abhor trial-and-error programming.
wenzelm@18537
    48
% They suggest that no one should write a program without First writing a complete
wenzelm@18537
    49
% formal specification. But university departments are not software houses. Programs like
wenzelm@18537
    50
% Isabelle are not products: when they have served their purpose, they are discarded.
wenzelm@18537
    51
%
wenzelm@18554
    52
% L.C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
wenzelm@18554
    53
wenzelm@18554
    54
% As I did 20 years ago, I still fervently believe that the only way to
wenzelm@18554
    55
% make software secure, reliable, and fast is to make it small. Fight
wenzelm@18554
    56
% Features.
wenzelm@18554
    57
%
wenzelm@18554
    58
% Andrew S. Tanenbaum
wenzelm@18537
    59
wenzelm@18537
    60
\appendix
wenzelm@18537
    61
\input{Thy/document/ML.tex}
wenzelm@18537
    62
wenzelm@18537
    63
\begingroup
wenzelm@18537
    64
\tocentry{\bibname}
wenzelm@18537
    65
\bibliographystyle{plain} \small\raggedright\frenchspacing
wenzelm@18537
    66
\bibliography{../manual}
wenzelm@18537
    67
\endgroup
wenzelm@18537
    68
wenzelm@18537
    69
\tocentry{\glossaryname}
wenzelm@18537
    70
\printglossary
wenzelm@18537
    71
wenzelm@18537
    72
\tocentry{\indexname}
wenzelm@18537
    73
\printindex
wenzelm@18537
    74
wenzelm@18537
    75
\end{document}
wenzelm@18537
    76
wenzelm@18537
    77
wenzelm@18537
    78
%%% Local Variables: 
wenzelm@18537
    79
%%% mode: latex
wenzelm@18537
    80
%%% TeX-master: t
wenzelm@18537
    81
%%% End: