doc-src/IsarImplementation/implementation.tex
author wenzelm
Sun May 01 16:36:34 2011 +0200 (2011-05-01)
changeset 42511 bf89455ccf9d
parent 39884 a16b18fd6299
child 42620 3a9723fca75c
permissions -rw-r--r--
eliminated copies of isabelle style files;
wenzelm@18537
     1
\documentclass[12pt,a4paper,fleqn]{report}
wenzelm@18537
     2
\usepackage{latexsym,graphicx}
wenzelm@18537
     3
\usepackage[refpage]{nomencl}
wenzelm@18537
     4
\usepackage{../iman,../extra,../isar,../proof}
wenzelm@26862
     5
\usepackage[nohyphen,strings]{../underscore}
wenzelm@42511
     6
\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
wenzelm@39827
     7
\usepackage{../ttbox,../rail,../railsetup}
wenzelm@18537
     8
\usepackage{style}
wenzelm@18537
     9
\usepackage{../pdfsetup}
wenzelm@18537
    10
wenzelm@18537
    11
wenzelm@18537
    12
\hyphenation{Isabelle}
wenzelm@18537
    13
\hyphenation{Isar}
wenzelm@18537
    14
wenzelm@18537
    15
\isadroptag{theory}
wenzelm@18537
    16
\title{\includegraphics[scale=0.5]{isabelle_isar}
wenzelm@18537
    17
  \\[4ex] The Isabelle/Isar Implementation}
wenzelm@28780
    18
\author{\emph{Makarius Wenzel}  \\[3ex]
wenzelm@28780
    19
  With Contributions by
wenzelm@28780
    20
  Florian Haftmann
wenzelm@28780
    21
  and Larry Paulson
wenzelm@28780
    22
}
wenzelm@18537
    23
wenzelm@18537
    24
\makeindex
wenzelm@18537
    25
wenzelm@39827
    26
\railterm{lbrace,rbrace,atsign}
wenzelm@39827
    27
\railalias{lbracesym}{\isasymlbrace}\railterm{lbracesym}
wenzelm@39827
    28
\railalias{rbracesym}{\isasymrbrace}\railterm{rbracesym}
wenzelm@39827
    29
\railalias{dots}{\isasymdots}\railterm{dots}
wenzelm@39827
    30
wenzelm@18537
    31
wenzelm@18537
    32
\begin{document}
wenzelm@18537
    33
wenzelm@35031
    34
\maketitle
wenzelm@18537
    35
wenzelm@18537
    36
\begin{abstract}
wenzelm@18537
    37
  We describe the key concepts underlying the Isabelle/Isar
wenzelm@18537
    38
  implementation, including ML references for the most important
wenzelm@20451
    39
  functions.  The aim is to give some insight into the overall system
wenzelm@20488
    40
  architecture, and provide clues on implementing applications within
wenzelm@20488
    41
  this framework.
wenzelm@18537
    42
\end{abstract}
wenzelm@18537
    43
wenzelm@19189
    44
\vspace*{2.5cm}
wenzelm@19189
    45
\begin{quote}
wenzelm@35031
    46
wenzelm@19189
    47
  {\small\em Isabelle was not designed; it evolved.  Not everyone
wenzelm@19189
    48
    likes this idea.  Specification experts rightly abhor
wenzelm@19189
    49
    trial-and-error programming.  They suggest that no one should
wenzelm@20024
    50
    write a program without first writing a complete formal
wenzelm@19189
    51
    specification. But university departments are not software houses.
wenzelm@19189
    52
    Programs like Isabelle are not products: when they have served
wenzelm@19189
    53
    their purpose, they are discarded.}
wenzelm@35031
    54
wenzelm@19189
    55
  Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
wenzelm@19189
    56
wenzelm@19189
    57
  \vspace*{1cm}
wenzelm@35031
    58
wenzelm@19189
    59
  {\small\em As I did 20 years ago, I still fervently believe that the
wenzelm@19189
    60
    only way to make software secure, reliable, and fast is to make it
wenzelm@20064
    61
    small.  Fight features.}
wenzelm@35031
    62
wenzelm@19189
    63
  Andrew S. Tanenbaum
wenzelm@19189
    64
wenzelm@35031
    65
  \vspace*{1cm}
wenzelm@35031
    66
wenzelm@35031
    67
  {\small\em One thing that UNIX does not need is more features. It is
wenzelm@35031
    68
    successful in part because it has a small number of good ideas
wenzelm@35031
    69
    that work well together. Merely adding features does not make it
wenzelm@35031
    70
    easier for users to do things --- it just makes the manual
wenzelm@35031
    71
    thicker. The right solution in the right place is always more
wenzelm@35031
    72
    effective than haphazard hacking.}
wenzelm@35031
    73
wenzelm@35031
    74
  Rob Pike and Brian W. Kernighan
wenzelm@35031
    75
wenzelm@19189
    76
\end{quote}
wenzelm@19189
    77
wenzelm@19189
    78
\thispagestyle{empty}\clearpage
wenzelm@19189
    79
wenzelm@20514
    80
\pagenumbering{roman}
wenzelm@20514
    81
\tableofcontents
wenzelm@20514
    82
\listoffigures
wenzelm@20514
    83
\clearfirst
wenzelm@18537
    84
wenzelm@39822
    85
\setcounter{chapter}{-1}
wenzelm@39822
    86
wenzelm@39822
    87
\input{Thy/document/ML.tex}
wenzelm@29755
    88
\input{Thy/document/Prelim.tex}
wenzelm@29755
    89
\input{Thy/document/Logic.tex}
wenzelm@39852
    90
\input{Thy/document/Syntax.tex}
wenzelm@29755
    91
\input{Thy/document/Tactic.tex}
wenzelm@29755
    92
\input{Thy/document/Proof.tex}
wenzelm@29755
    93
\input{Thy/document/Isar.tex}
wenzelm@29755
    94
\input{Thy/document/Local_Theory.tex}
wenzelm@29755
    95
\input{Thy/document/Integration.tex}
wenzelm@18537
    96
wenzelm@18537
    97
\begingroup
wenzelm@18537
    98
\tocentry{\bibname}
wenzelm@30116
    99
\bibliographystyle{abbrv} \small\raggedright\frenchspacing
wenzelm@18537
   100
\bibliography{../manual}
wenzelm@18537
   101
\endgroup
wenzelm@18537
   102
wenzelm@18537
   103
\tocentry{\indexname}
wenzelm@18537
   104
\printindex
wenzelm@18537
   105
wenzelm@18537
   106
\end{document}
wenzelm@18537
   107
wenzelm@18537
   108
wenzelm@35031
   109
%%% Local Variables:
wenzelm@18537
   110
%%% mode: latex
wenzelm@18537
   111
%%% TeX-master: t
wenzelm@35031
   112
%%% End: