doc-src/IsarOverview/Isar/document/root.tex
author wenzelm
Tue, 10 Jun 2008 19:15:16 +0200
changeset 27123 11fcdd5897dd
parent 26911 871cc7f11034
child 42511 bf89455ccf9d
permissions -rw-r--r--
case_tac/induct_tac: use same declarations as cases/induct;

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

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

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

\pagestyle{plain}

\begin{document}

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

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

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

\end{document}