--- a/src/Doc/Codegen/Introduction.thy Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/Codegen/Introduction.thy Fri Dec 16 18:11:03 2022 +0100
@@ -222,6 +222,9 @@
dramatically by applying refinement techniques, which are
introduced in \secref{sec:refinement}.
+ \item How to define partial functions such that code can be generated
+ is explained in \secref{sec:partial}.
+
\item Inductive predicates can be turned executable using an
extension of the code generator \secref{sec:inductive}.
--- a/src/Doc/Codegen/document/root.tex Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/Codegen/document/root.tex Fri Dec 16 18:11:03 2022 +0100
@@ -15,7 +15,7 @@
\title{\includegraphics[scale=0.5]{isabelle_logo}
\\[4ex] Code generation from Isabelle/HOL theories}
-\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
+\author{\emph{Florian Haftmann}\\ with contributions by Lukas Bulwahn and Tobias Nipkow}
\begin{document}
@@ -35,6 +35,7 @@
\input{Introduction.tex}
\input{Foundations.tex}
\input{Refinement.tex}
+\input{Partial_Functions.tex}
\input{Inductive_Predicate.tex}
\input{Evaluation.tex}
\input{Computations.tex}
--- a/src/Doc/Functions/Functions.thy Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/Functions/Functions.thy Fri Dec 16 18:11:03 2022 +0100
@@ -750,7 +750,7 @@
termination by (relation "{}") simp
-section \<open>Partiality\<close>
+section \<open>Partiality \label{sec:partiality}\<close>
text \<open>
In HOL, all functions are total. A function \<^term>\<open>f\<close> applied to
--- a/src/Doc/Functions/document/intro.tex Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/Functions/document/intro.tex Fri Dec 16 18:11:03 2022 +0100
@@ -43,8 +43,6 @@
to existing principles.
-
-
The new \cmd{function} command, and its short form \cmd{fun} have mostly
replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
a few of technical issues around \cmd{recdef}, and allow definitions
@@ -52,6 +50,10 @@
In addition there is also the \cmd{partial\_function} command
(see \cite{isabelle-isar-ref}) that supports the definition of partial
-and tail recursive functions.
+and tail recursive functions. This command is particulary relevant if one wants to
+generate executable code. This is covered in detail in the Code Generation
+tutorial~\cite{Haftmann-codegen}.
+The approach to partial function presented in Section~\ref{sec:partiality}
+of this tutorial does not support code generation.
--- a/src/Doc/ROOT Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/ROOT Fri Dec 16 18:11:03 2022 +0100
@@ -26,6 +26,7 @@
Introduction
Foundations
Refinement
+ Partial_Functions
Inductive_Predicate
Evaluation
Computations
--- a/src/Doc/manual.bib Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/manual.bib Fri Dec 16 18:11:03 2022 +0100
@@ -827,6 +827,10 @@
%H
+@manual{Haftmann-codegen,author={Florian Haftmann},
+title={Code generation from {Isabelle/HOL} theories},
+note={\url{http://isabelle.in.tum.de/doc/codegen.pdf}}}
+
@inproceedings{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement,
author = {Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow},
title = {Data Refinement in {Isabelle/HOL}},