doc-src/IsarImplementation/implementation.tex
author wenzelm
Thu, 31 May 2007 14:34:07 +0200
changeset 23156 6ec9e29143e9
parent 22868 c82dd66560ac
child 26854 9b4aec46ad78
permissions -rw-r--r--
removed obsolete IFOL.thy/FOL.thy values;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     1
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     2
%% $Id$
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     3
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
\documentclass[12pt,a4paper,fleqn]{report}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
\usepackage{latexsym,graphicx}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
\usepackage[refpage]{nomencl}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     7
\usepackage{../iman,../extra,../isar,../proof}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     8
\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     9
\usepackage{style}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    10
\usepackage{../pdfsetup}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    11
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    12
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    13
\hyphenation{Isabelle}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    14
\hyphenation{Isar}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    15
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    16
\isadroptag{theory}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    17
\title{\includegraphics[scale=0.5]{isabelle_isar}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    18
  \\[4ex] The Isabelle/Isar Implementation}
20024
wenzelm
parents: 19189
diff changeset
    19
\author{\emph{Makarius Wenzel}}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    20
20475
wenzelm
parents: 20472
diff changeset
    21
%FIXME
wenzelm
parents: 20472
diff changeset
    22
%\makeglossary
wenzelm
parents: 20472
diff changeset
    23
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    24
\makeindex
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    25
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    26
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    27
\begin{document}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    28
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    29
\maketitle 
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    30
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    31
\begin{abstract}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    32
  We describe the key concepts underlying the Isabelle/Isar
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    33
  implementation, including ML references for the most important
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20064
diff changeset
    34
  functions.  The aim is to give some insight into the overall system
20488
wenzelm
parents: 20475
diff changeset
    35
  architecture, and provide clues on implementing applications within
wenzelm
parents: 20475
diff changeset
    36
  this framework.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    37
\end{abstract}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    38
19189
wenzelm
parents: 18554
diff changeset
    39
\vspace*{2.5cm}
wenzelm
parents: 18554
diff changeset
    40
\begin{quote}
wenzelm
parents: 18554
diff changeset
    41
  
wenzelm
parents: 18554
diff changeset
    42
  {\small\em Isabelle was not designed; it evolved.  Not everyone
wenzelm
parents: 18554
diff changeset
    43
    likes this idea.  Specification experts rightly abhor
wenzelm
parents: 18554
diff changeset
    44
    trial-and-error programming.  They suggest that no one should
20024
wenzelm
parents: 19189
diff changeset
    45
    write a program without first writing a complete formal
19189
wenzelm
parents: 18554
diff changeset
    46
    specification. But university departments are not software houses.
wenzelm
parents: 18554
diff changeset
    47
    Programs like Isabelle are not products: when they have served
wenzelm
parents: 18554
diff changeset
    48
    their purpose, they are discarded.}
wenzelm
parents: 18554
diff changeset
    49
  
wenzelm
parents: 18554
diff changeset
    50
  Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
wenzelm
parents: 18554
diff changeset
    51
wenzelm
parents: 18554
diff changeset
    52
  \vspace*{1cm}
wenzelm
parents: 18554
diff changeset
    53
  
wenzelm
parents: 18554
diff changeset
    54
  {\small\em As I did 20 years ago, I still fervently believe that the
wenzelm
parents: 18554
diff changeset
    55
    only way to make software secure, reliable, and fast is to make it
20064
wenzelm
parents: 20024
diff changeset
    56
    small.  Fight features.}
19189
wenzelm
parents: 18554
diff changeset
    57
  
wenzelm
parents: 18554
diff changeset
    58
  Andrew S. Tanenbaum
wenzelm
parents: 18554
diff changeset
    59
wenzelm
parents: 18554
diff changeset
    60
\end{quote}
wenzelm
parents: 18554
diff changeset
    61
wenzelm
parents: 18554
diff changeset
    62
\thispagestyle{empty}\clearpage
wenzelm
parents: 18554
diff changeset
    63
20514
5ede702cd2ca more on terms;
wenzelm
parents: 20488
diff changeset
    64
\pagenumbering{roman}
5ede702cd2ca more on terms;
wenzelm
parents: 20488
diff changeset
    65
\tableofcontents
5ede702cd2ca more on terms;
wenzelm
parents: 20488
diff changeset
    66
\listoffigures
5ede702cd2ca more on terms;
wenzelm
parents: 20488
diff changeset
    67
\clearfirst
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    68
22868
wenzelm
parents: 20514
diff changeset
    69
%\input{intro.tex}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    70
\input{Thy/document/prelim.tex}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    71
\input{Thy/document/logic.tex}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    72
\input{Thy/document/tactic.tex}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    73
\input{Thy/document/proof.tex}
20472
wenzelm
parents: 20451
diff changeset
    74
\input{Thy/document/isar.tex}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    75
\input{Thy/document/locale.tex}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    76
\input{Thy/document/integration.tex}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    77
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    78
\appendix
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    79
\input{Thy/document/ML.tex}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    80
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    81
\begingroup
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    82
\tocentry{\bibname}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    83
\bibliographystyle{plain} \small\raggedright\frenchspacing
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    84
\bibliography{../manual}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    85
\endgroup
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    86
20475
wenzelm
parents: 20472
diff changeset
    87
%FIXME
wenzelm
parents: 20472
diff changeset
    88
%\tocentry{\glossaryname}
wenzelm
parents: 20472
diff changeset
    89
%\printglossary
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    90
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    91
\tocentry{\indexname}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    92
\printindex
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    93
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    94
\end{document}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    95
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    96
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    97
%%% Local Variables: 
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    98
%%% mode: latex
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    99
%%% TeX-master: t
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   100
%%% End: