doc-src/IsarImplementation/implementation.tex
author wenzelm
Tue Sep 19 23:15:28 2006 +0200 (2006-09-19)
changeset 20622 e1a573146be5
parent 20514 5ede702cd2ca
child 22868 c82dd66560ac
permissions -rw-r--r--
tuned proofs;
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@20024
    19
\author{\emph{Makarius Wenzel}}
wenzelm@18537
    20
wenzelm@20475
    21
%FIXME
wenzelm@20475
    22
%\makeglossary
wenzelm@20475
    23
wenzelm@18537
    24
\makeindex
wenzelm@18537
    25
wenzelm@18537
    26
wenzelm@18537
    27
\begin{document}
wenzelm@18537
    28
wenzelm@18537
    29
\maketitle 
wenzelm@18537
    30
wenzelm@18537
    31
\begin{abstract}
wenzelm@18537
    32
  We describe the key concepts underlying the Isabelle/Isar
wenzelm@18537
    33
  implementation, including ML references for the most important
wenzelm@20451
    34
  functions.  The aim is to give some insight into the overall system
wenzelm@20488
    35
  architecture, and provide clues on implementing applications within
wenzelm@20488
    36
  this framework.
wenzelm@18537
    37
\end{abstract}
wenzelm@18537
    38
wenzelm@19189
    39
\vspace*{2.5cm}
wenzelm@19189
    40
\begin{quote}
wenzelm@19189
    41
  
wenzelm@19189
    42
  {\small\em Isabelle was not designed; it evolved.  Not everyone
wenzelm@19189
    43
    likes this idea.  Specification experts rightly abhor
wenzelm@19189
    44
    trial-and-error programming.  They suggest that no one should
wenzelm@20024
    45
    write a program without first writing a complete formal
wenzelm@19189
    46
    specification. But university departments are not software houses.
wenzelm@19189
    47
    Programs like Isabelle are not products: when they have served
wenzelm@19189
    48
    their purpose, they are discarded.}
wenzelm@19189
    49
  
wenzelm@19189
    50
  Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
wenzelm@19189
    51
wenzelm@19189
    52
  \vspace*{1cm}
wenzelm@19189
    53
  
wenzelm@19189
    54
  {\small\em As I did 20 years ago, I still fervently believe that the
wenzelm@19189
    55
    only way to make software secure, reliable, and fast is to make it
wenzelm@20064
    56
    small.  Fight features.}
wenzelm@19189
    57
  
wenzelm@19189
    58
  Andrew S. Tanenbaum
wenzelm@19189
    59
wenzelm@19189
    60
\end{quote}
wenzelm@19189
    61
wenzelm@19189
    62
\thispagestyle{empty}\clearpage
wenzelm@19189
    63
wenzelm@20514
    64
\pagenumbering{roman}
wenzelm@20514
    65
\tableofcontents
wenzelm@20514
    66
\listoffigures
wenzelm@20514
    67
\clearfirst
wenzelm@18537
    68
wenzelm@18537
    69
\input{intro.tex}
wenzelm@18537
    70
\input{Thy/document/prelim.tex}
wenzelm@18537
    71
\input{Thy/document/logic.tex}
wenzelm@18537
    72
\input{Thy/document/tactic.tex}
wenzelm@18537
    73
\input{Thy/document/proof.tex}
wenzelm@20472
    74
\input{Thy/document/isar.tex}
wenzelm@18537
    75
\input{Thy/document/locale.tex}
wenzelm@18537
    76
\input{Thy/document/integration.tex}
wenzelm@18537
    77
wenzelm@18537
    78
\appendix
wenzelm@18537
    79
\input{Thy/document/ML.tex}
wenzelm@18537
    80
wenzelm@18537
    81
\begingroup
wenzelm@18537
    82
\tocentry{\bibname}
wenzelm@18537
    83
\bibliographystyle{plain} \small\raggedright\frenchspacing
wenzelm@18537
    84
\bibliography{../manual}
wenzelm@18537
    85
\endgroup
wenzelm@18537
    86
wenzelm@20475
    87
%FIXME
wenzelm@20475
    88
%\tocentry{\glossaryname}
wenzelm@20475
    89
%\printglossary
wenzelm@18537
    90
wenzelm@18537
    91
\tocentry{\indexname}
wenzelm@18537
    92
\printindex
wenzelm@18537
    93
wenzelm@18537
    94
\end{document}
wenzelm@18537
    95
wenzelm@18537
    96
wenzelm@18537
    97
%%% Local Variables: 
wenzelm@18537
    98
%%% mode: latex
wenzelm@18537
    99
%%% TeX-master: t
wenzelm@18537
   100
%%% End: