wenzelm@18537: \documentclass[12pt,a4paper,fleqn]{report}
wenzelm@18537: \usepackage{latexsym,graphicx}
wenzelm@18537: \usepackage[refpage]{nomencl}
wenzelm@18537: \usepackage{../iman,../extra,../isar,../proof}
wenzelm@26862: \usepackage[nohyphen,strings]{../underscore}
wenzelm@26906: \usepackage{../isabelle,../isabellesym}
wenzelm@18537: \usepackage{style}
wenzelm@18537: \usepackage{../pdfsetup}
wenzelm@18537: 
wenzelm@18537: 
wenzelm@18537: \hyphenation{Isabelle}
wenzelm@18537: \hyphenation{Isar}
wenzelm@18537: 
wenzelm@18537: \isadroptag{theory}
wenzelm@18537: \title{\includegraphics[scale=0.5]{isabelle_isar}
wenzelm@18537:   \\[4ex] The Isabelle/Isar Implementation}
wenzelm@28780: \author{\emph{Makarius Wenzel}  \\[3ex]
wenzelm@28780:   With Contributions by
wenzelm@28780:   Florian Haftmann
wenzelm@28780:   and Larry Paulson
wenzelm@28780: }
wenzelm@18537: 
wenzelm@18537: \makeindex
wenzelm@18537: 
wenzelm@18537: 
wenzelm@18537: \begin{document}
wenzelm@18537: 
wenzelm@35031: \maketitle
wenzelm@18537: 
wenzelm@18537: \begin{abstract}
wenzelm@18537:   We describe the key concepts underlying the Isabelle/Isar
wenzelm@18537:   implementation, including ML references for the most important
wenzelm@20451:   functions.  The aim is to give some insight into the overall system
wenzelm@20488:   architecture, and provide clues on implementing applications within
wenzelm@20488:   this framework.
wenzelm@18537: \end{abstract}
wenzelm@18537: 
wenzelm@19189: \vspace*{2.5cm}
wenzelm@19189: \begin{quote}
wenzelm@35031: 
wenzelm@19189:   {\small\em Isabelle was not designed; it evolved.  Not everyone
wenzelm@19189:     likes this idea.  Specification experts rightly abhor
wenzelm@19189:     trial-and-error programming.  They suggest that no one should
wenzelm@20024:     write a program without first writing a complete formal
wenzelm@19189:     specification. But university departments are not software houses.
wenzelm@19189:     Programs like Isabelle are not products: when they have served
wenzelm@19189:     their purpose, they are discarded.}
wenzelm@35031: 
wenzelm@19189:   Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
wenzelm@19189: 
wenzelm@19189:   \vspace*{1cm}
wenzelm@35031: 
wenzelm@19189:   {\small\em As I did 20 years ago, I still fervently believe that the
wenzelm@19189:     only way to make software secure, reliable, and fast is to make it
wenzelm@20064:     small.  Fight features.}
wenzelm@35031: 
wenzelm@19189:   Andrew S. Tanenbaum
wenzelm@19189: 
wenzelm@35031:   \vspace*{1cm}
wenzelm@35031: 
wenzelm@35031:   {\small\em One thing that UNIX does not need is more features. It is
wenzelm@35031:     successful in part because it has a small number of good ideas
wenzelm@35031:     that work well together. Merely adding features does not make it
wenzelm@35031:     easier for users to do things --- it just makes the manual
wenzelm@35031:     thicker. The right solution in the right place is always more
wenzelm@35031:     effective than haphazard hacking.}
wenzelm@35031: 
wenzelm@35031:   Rob Pike and Brian W. Kernighan
wenzelm@35031: 
wenzelm@19189: \end{quote}
wenzelm@19189: 
wenzelm@19189: \thispagestyle{empty}\clearpage
wenzelm@19189: 
wenzelm@20514: \pagenumbering{roman}
wenzelm@20514: \tableofcontents
wenzelm@20514: \listoffigures
wenzelm@20514: \clearfirst
wenzelm@18537: 
wenzelm@30081: \input{Thy/document/Prelim.tex}
wenzelm@30081: \input{Thy/document/Logic.tex}
wenzelm@30081: \input{Thy/document/Tactic.tex}
wenzelm@30081: \input{Thy/document/Proof.tex}
wenzelm@30124: \input{Thy/document/Syntax.tex}
wenzelm@30081: \input{Thy/document/Isar.tex}
wenzelm@30081: \input{Thy/document/Local_Theory.tex}
wenzelm@30081: \input{Thy/document/Integration.tex}
wenzelm@18537: 
wenzelm@18537: \appendix
wenzelm@18537: \input{Thy/document/ML.tex}
wenzelm@18537: 
wenzelm@18537: \begingroup
wenzelm@18537: \tocentry{\bibname}
wenzelm@30114: \bibliographystyle{abbrv} \small\raggedright\frenchspacing
wenzelm@18537: \bibliography{../manual}
wenzelm@18537: \endgroup
wenzelm@18537: 
wenzelm@18537: \tocentry{\indexname}
wenzelm@18537: \printindex
wenzelm@18537: 
wenzelm@18537: \end{document}
wenzelm@18537: 
wenzelm@18537: 
wenzelm@35031: %%% Local Variables:
wenzelm@18537: %%% mode: latex
wenzelm@18537: %%% TeX-master: t
wenzelm@35031: %%% End: