src/Doc/IsarImplementation/document/root.tex

yet another attempt at actual underscore;
enforce scalable fonts for T1 encoding;

\documentclass[12pt,a4paper,fleqn]{report}
\usepackage[T1]{fontenc}
\usepackage{ae}
\usepackage{latexsym,graphicx}
\usepackage[refpage]{nomencl}
\usepackage{iman,extra,isar,proof}
\usepackage[nohyphen,strings]{underscore}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{railsetup}
\usepackage{ttbox}
\usepackage{supertabular}
\usepackage{style}
\usepackage{pdfsetup}


\hyphenation{Isabelle}
\hyphenation{Isar}

\isadroptag{theory}
\title{\includegraphics[scale=0.5]{isabelle_isar}
  \\[4ex] The Isabelle/Isar Implementation}
\author{\emph{Makarius Wenzel}  \\[3ex]
  With Contributions by
  Stefan Berghofer, \\
  Florian Haftmann
  and Larry Paulson
}

\makeindex


\begin{document}

\maketitle

\begin{abstract}
  We describe the key concepts underlying the Isabelle/Isar
  implementation, including ML references for the most important
  functions.  The aim is to give some insight into the overall system
  architecture, and provide clues on implementing applications within
  this framework.
\end{abstract}

\vspace*{2.5cm}
\begin{quote}

  {\small\em Isabelle was not designed; it evolved.  Not everyone
    likes this idea.  Specification experts rightly abhor
    trial-and-error programming.  They suggest that no one should
    write a program without first writing a complete formal
    specification. But university departments are not software houses.
    Programs like Isabelle are not products: when they have served
    their purpose, they are discarded.}

  Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''

  \vspace*{1cm}

  {\small\em As I did 20 years ago, I still fervently believe that the
    only way to make software secure, reliable, and fast is to make it
    small.  Fight features.}

  Andrew S. Tanenbaum

  \vspace*{1cm}

  {\small\em One thing that UNIX does not need is more features. It is
    successful in part because it has a small number of good ideas
    that work well together. Merely adding features does not make it
    easier for users to do things --- it just makes the manual
    thicker. The right solution in the right place is always more
    effective than haphazard hacking.}

  Rob Pike and Brian W. Kernighan

  \vspace*{1cm}

  {\small\em If you look at software today, through the lens of the
    history of engineering, it's certainly engineering of a sort--but
    it's the kind of engineering that people without the concept of
    the arch did. Most software today is very much like an Egyptian
    pyramid with millions of bricks piled on top of each other, with
    no structural integrity, but just done by brute force and
    thousands of slaves.}

  Alan Kay

\end{quote}

\thispagestyle{empty}\clearpage

\pagenumbering{roman}
\tableofcontents
\listoffigures
\clearfirst

\setcounter{chapter}{-1}

\input{ML.tex}
\input{Prelim.tex}
\input{Logic.tex}
\input{Syntax.tex}
\input{Tactic.tex}
\input{Eq.tex}
\input{Proof.tex}
\input{Isar.tex}
\input{Local_Theory.tex}
\input{Integration.tex}

\begingroup
\tocentry{\bibname}
\bibliographystyle{abbrv} \small\raggedright\frenchspacing
\bibliography{manual}
\endgroup

\tocentry{\indexname}
\printindex

\end{document}


%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: