--- a/doc-src/Codegen/Thy/Further.thy Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/Thy/Further.thy Wed Nov 03 14:14:06 2010 +0100
@@ -124,7 +124,8 @@
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
\cite{bulwahn-et-al:2008:imperative}; the framework described there
- is available in session @{text Imperative_HOL}.
+ is available in session @{text Imperative_HOL}, together with a short
+ primer document.
*}
--- a/doc-src/Codegen/Thy/Refinement.thy Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/Thy/Refinement.thy Wed Nov 03 14:14:06 2010 +0100
@@ -17,7 +17,7 @@
text {*
Program refinement works by choosing appropriate code equations
- explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+ explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci
numbers:
*}
--- a/doc-src/Codegen/Thy/document/Further.tex Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex Wed Nov 03 14:14:06 2010 +0100
@@ -240,7 +240,8 @@
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
\cite{bulwahn-et-al:2008:imperative}; the framework described there
- is available in session \isa{Imperative{\isacharunderscore}HOL}.%
+ is available in session \isa{Imperative{\isacharunderscore}HOL}, together with a short
+ primer document.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Refinement.tex Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Wed Nov 03 14:14:06 2010 +0100
@@ -37,7 +37,7 @@
%
\begin{isamarkuptext}%
Program refinement works by choosing appropriate code equations
- explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+ explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci
numbers:%
\end{isamarkuptext}%
\isamarkuptrue%