1 2% HOLCF/document/root.tex 3 4\documentclass[11pt,a4paper]{article} 5\usepackage{graphicx,isabelle,isabellesym,latexsym} 6\usepackage[only,bigsqcap]{stmaryrd} 7\usepackage{textcomp} 8\usepackage{pdfsetup} 9 10\urlstyle{rm} 11\isabellestyle{it} 12\pagestyle{myheadings} 13\newcommand{\isasymas}{\textsf{as}} 14\newcommand{\isasymlazy}{\isamath{\sim}} 15\newcommand{\isasymnotsqsubseteq}{\isamath{\not\sqsubseteq}} 16 17\begin{document} 18 19\title{Isabelle/HOLCF --- Higher-Order Logic of Computable Functions} 20\maketitle 21 22\tableofcontents 23 24\begin{center} 25 \includegraphics[scale=0.45]{session_graph} 26\end{center} 27 28\newpage 29 30\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}} 31 32\parindent 0pt\parskip 0.5ex 33\input{session} 34 35\end{document} 36