\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: