
\chapter{The Isabelle/Isar Conversion Guide}

\section{No conversion}

FIXME thm, theory, bind_thm(s);


\section{Porting proof scripts}

\section{Performing actual proof}

FIXME


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "isar-ref"
%%% End: 
