doc-src/IsarImplementation/implementation.tex
author wenzelm
Thu Aug 31 22:55:49 2006 +0200 (2006-08-31 ago)
changeset 20451 27ea2ba48fa3
parent 20064 92aad017b847
child 20472 e993073eda4c
permissions -rw-r--r--
misc cleanup;
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@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@20451
    32
  functions.  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@19189
    36
\vspace*{2.5cm}
wenzelm@19189
    37
\begin{quote}
wenzelm@19189
    38
  
wenzelm@19189
    39
  {\small\em Isabelle was not designed; it evolved.  Not everyone
wenzelm@19189
    40
    likes this idea.  Specification experts rightly abhor
wenzelm@19189
    41
    trial-and-error programming.  They suggest that no one should
wenzelm@20024
    42
    write a program without first writing a complete formal
wenzelm@19189
    43
    specification. But university departments are not software houses.
wenzelm@19189
    44
    Programs like Isabelle are not products: when they have served
wenzelm@19189
    45
    their purpose, they are discarded.}
wenzelm@19189
    46
  
wenzelm@19189
    47
  Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
wenzelm@19189
    48
wenzelm@19189
    49
  \vspace*{1cm}
wenzelm@19189
    50
  
wenzelm@19189
    51
  {\small\em As I did 20 years ago, I still fervently believe that the
wenzelm@19189
    52
    only way to make software secure, reliable, and fast is to make it
wenzelm@20064
    53
    small.  Fight features.}
wenzelm@19189
    54
  
wenzelm@19189
    55
  Andrew S. Tanenbaum
wenzelm@19189
    56
wenzelm@19189
    57
\end{quote}
wenzelm@19189
    58
wenzelm@19189
    59
\thispagestyle{empty}\clearpage
wenzelm@19189
    60
wenzelm@18537
    61
\pagenumbering{roman} \tableofcontents \clearfirst
wenzelm@18537
    62
wenzelm@18537
    63
\input{intro.tex}
wenzelm@18537
    64
\input{Thy/document/prelim.tex}
wenzelm@18537
    65
\input{Thy/document/logic.tex}
wenzelm@18537
    66
\input{Thy/document/tactic.tex}
wenzelm@18537
    67
\input{Thy/document/proof.tex}
wenzelm@18537
    68
\input{Thy/document/locale.tex}
wenzelm@18537
    69
\input{Thy/document/integration.tex}
wenzelm@18537
    70
wenzelm@18537
    71
\appendix
wenzelm@18537
    72
\input{Thy/document/ML.tex}
wenzelm@18537
    73
wenzelm@18537
    74
\begingroup
wenzelm@18537
    75
\tocentry{\bibname}
wenzelm@18537
    76
\bibliographystyle{plain} \small\raggedright\frenchspacing
wenzelm@18537
    77
\bibliography{../manual}
wenzelm@18537
    78
\endgroup
wenzelm@18537
    79
wenzelm@18537
    80
\tocentry{\glossaryname}
wenzelm@18537
    81
\printglossary
wenzelm@18537
    82
wenzelm@18537
    83
\tocentry{\indexname}
wenzelm@18537
    84
\printindex
wenzelm@18537
    85
wenzelm@18537
    86
\end{document}
wenzelm@18537
    87
wenzelm@18537
    88
wenzelm@18537
    89
%%% Local Variables: 
wenzelm@18537
    90
%%% mode: latex
wenzelm@18537
    91
%%% TeX-master: t
wenzelm@18537
    92
%%% End: