added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
% HOLCF/document/root.tex
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx,isabelle,isabellesym,latexsym}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{textcomp}
\usepackage{pdfsetup}
\urlstyle{rm}
%\isabellestyle{it}
\pagestyle{myheadings}
\begin{document}
\title{Isabelle/HOLCF Tutorial}
\maketitle
\tableofcontents
%\newpage
%\renewcommand{\isamarkupheader}[1]%
%{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
\parindent 0pt\parskip 0.5ex
\input{session}
\end{document}