doc-src/TutorialI/Overview/document/root.tex

fixed subgoal_tac; fails on non-existent subgoal;

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

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

\newtheorem{Exercise}{Exercise}[section]
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}

\begin{document}

\title{Overview}\maketitle

\input{session}

%\bibliographystyle{plain}
%\bibliography{root}

\end{document}