1\documentclass[12pt,a4paper]{article} % fleqn 2\usepackage{lmodern} 3\usepackage[T1]{fontenc} 4\usepackage{amsfonts} 5\usepackage{amsmath} 6\usepackage{cite} 7\usepackage{enumitem} 8\usepackage{footmisc} 9\usepackage{latexsym} 10\usepackage{graphicx} 11\usepackage{iman} 12\usepackage{extra} 13\usepackage{isar} 14\usepackage{isabelle} 15\usepackage{isabellesym} 16\usepackage{style} 17\usepackage{pdfsetup} 18\usepackage{railsetup} 19\usepackage{framed} 20\usepackage{regexpatch} 21 22\makeatletter 23\xpatchcmd{\chaptermark}{\MakeUppercase}{}{}{}% 24\xpatchcmd{\sectionmark}{\MakeUppercase}{}{}{}% 25\xpatchcmd*{\tableofcontents}{\MakeUppercase}{}{}{}% 26\makeatother 27 28\setcounter{secnumdepth}{3} 29\setcounter{tocdepth}{3} 30 31\renewcommand\_{\hbox{\textunderscore\kern-.05ex}} 32 33\newbox\boxA 34\setbox\boxA=\hbox{\ } 35\parindent=4\wd\boxA 36 37\newcommand\blankline{\vskip-.25\baselineskip} 38 39\newenvironment{indentblock}{\list{}{\setlength{\leftmargin}{\parindent}}\item[]}{\endlist} 40 41\newcommand{\keyw}[1]{\textbf{#1}} 42\newcommand{\synt}[1]{\textit{#1}} 43\newcommand{\hthm}[1]{\textbf{\textit{#1}}} 44 45%\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$} 46\renewcommand\isactrlsub[1]{\/$\sb{#1}$} 47\renewcommand\isadigit[1]{\/\ensuremath{\mathrm{#1}}} 48\renewcommand\isacharprime{\isamath{{'}\mskip-2mu}} 49\renewcommand\isacharunderscore{\mbox{\_}} 50\renewcommand\isacharunderscorekeyword{\mbox{\_}} 51\renewcommand\isachardoublequote{\mbox{\upshape{``}}} 52\renewcommand\isachardoublequoteopen{\mbox{\upshape{``}\kern.1ex}} 53\renewcommand\isachardoublequoteclose{\/\kern.15ex\mbox{\upshape{''}}} 54\renewcommand\isacharverbatimopen{\isacharbraceleft\isacharasterisk} 55\renewcommand\isacharverbatimclose{\isacharasterisk\isacharbraceright} 56\renewcommand{\isasyminverse}{\isamath{{}^{-}}} 57 58\hyphenation{isa-belle} 59 60\isadroptag{theory} 61 62\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] 63Defining Nonprimitively (Co)recursive Functions in Isabelle/HOL} 64\author{Jasmin Christian Blanchette, Aymeric Bouzy, \\ 65Andreas Lochbihler, Andrei Popescu, and \\ 66Dmitriy Traytel} 67 68\urlstyle{tt} 69 70\begin{document} 71 72\maketitle 73 74\begin{sloppy} 75\begin{abstract} 76\noindent 77This tutorial describes the definitional package for nonprimitively corecursive functions 78in Isabelle/HOL. The following commands are provided: 79\keyw{corec}, \keyw{corecursive}, \keyw{friend\_of\_corec}, and \keyw{coinduction\_\allowbreak upto}. 80They supplement \keyw{codatatype}, \keyw{primcorec}, and \keyw{primco\-rec\-ur\-sive}, which 81define codatatypes and primitively corecursive functions. 82\end{abstract} 83\end{sloppy} 84 85\tableofcontents 86 87\input{Corec.tex} 88 89\let\em=\sl 90\bibliography{manual}{} 91\bibliographystyle{abbrv} 92 93\end{document} 94