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

*** empty log message ***

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

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

\newcommand{\tweakskip}{\vspace{-\medskipamount}}
\newcommand{\Tweakskip}{\tweakskip\tweakskip}

\pagestyle{plain}

\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}
\Tweakskip\Tweakskip
\input{Induction.tex}

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

\end{document}