Manual/Tutorial/binomial.tex

%%%% Revised contents of Manual/Tutorial/binomial.tex %%%%
\chapter{Example: the Binomial Theorem}\label{binomial}

The Binomial Theorem in \HOL{} is a medium sized worked example whose subject
matter is more widely known than any specific piece of hardware or software.
This chapter introduces the small amount of algebra and mathematical notation
needed to state and prove the Binomial Theorem, shows how this is rendered
in \HOL{}, and outlines the structure of the proof.

This chapter is also available as the self-contained case study \ml{binomial}
in the directory {\small\verb%Training/studies%}.

\def\self{chapter}
\def\path{{\tt Training/studies/binomial}}
\input{binomial/binomial}
\input{binomial/appendix}