doc-src/TutorialI/IsarOverview/Isar/document/root.tex

Added mk_int and mk_list.

\documentclass[envcountsame]{llncs}
%\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}

%for best-style documents ...
\urlstyle{rm}
%\isabellestyle{it}

\begin{document}

\title{A Compact Introduction to Structured Proofs in Isar/HOL}
\author{Tobias Nipkow}
\institute{Institut f{\"u}r Informatik, TU M{\"u}nchen\\
 {\small\url{http://www.in.tum.de/~nipkow/}}}
\date{}
\maketitle

\begin{abstract}
  Isar is an extension of the theorem prover Isabelle with a language
  for writing human-readable structured proofs. This paper is an
  introduction to the basic constructs of this language. It is aimed
  at potential users of Isar but also discusses the design rationals
  behind the language and its constructs.
\end{abstract}

\input{intro.tex}
\input{Logic.tex}
\input{Induction.tex}

%\input{Isar.tex}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:

{\small
\paragraph{Acknowledgment}
I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer and
Markus Wenzel commented on and improved this document.
}

\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{root}
\endgroup

\end{document}