* Pure/TheoryDataFun: change of the argument structure;
* Pure/TheoryDataFun: change of the argument structure -- got rid of Sign.sg;
\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{A Compact Overview of Isabelle/HOL}
\author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\
\small\url{http://www.in.tum.de/~nipkow/}}
\date{}
\maketitle
\noindent
This document is a very compact introduction to the proof assistant
Isabelle/HOL and is based directly on the published tutorial~\cite{LNCS2283}
where full explanations and a wealth of additional material can be found.
While reading this document it is recommended to single-step through the
corresponding theories using Isabelle/HOL to follow the proofs.
\section{Functional Programming/Modelling}
\subsection{An Introductory Theory}
\input{FP0.tex}
\begin{exercise}
Define a datatype of binary trees and a function \isa{mirror}
that mirrors a binary tree by swapping subtrees recursively. Prove
\isa{mirror(mirror t) = t}.
Define a function \isa{flatten} that flattens a tree into a list
by traversing it in infix order. Prove
\isa{flatten(mirror t) = rev(flatten t)}.
\end{exercise}
\subsection{More Constructs}
\input{FP1.tex}
\input{RECDEF.tex}
\input{Rules.tex}
\input{Sets.tex}
\input{Ind.tex}
%\input{Isar.tex}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
\bibliographystyle{plain}
\bibliography{root}
\end{document}