% !TeX root = easycrypt.tex
\chapter{Structuring Specifications and Proofs}

One of the main improvements of \EasyCrypt1.0 over its predecessors is its
wealth of proof structuring mechanisms, which provide ways to abstract
irrelevant details away, reuse proofs, and concretely instantiate high-level
results. We described here the three main mechanisms:
\begin{inparaenum}
\item type classes, that allow the user to reason abstractly on types and
      functions;
\item theories and cloning, that allow the user to group sets of function and
      module definitions together with lemmas relevant to them and reuse
      them in various contexts; and
\item sections, that allows for a better isolation of proof artefacts.
\end{inparaenum}

\section{Type classes}
\warningbox{This feature is not yet implemented}

\section{Theories and cloning\label{sec:cloning}}

\section{Sections\label{sec:sections}}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "easycrypt"
%%% End: