# HG changeset patch
# User haftmann
# Date 1288790046 -3600
# Node ID 8fd36f8a5cb7c5bdf595c1bd18e0f85fea0c476a
# Parent  090dac52cfd78181f1757fa6a6dee670503cf3a9
more precise text

diff -r 090dac52cfd7 -r 8fd36f8a5cb7 doc-src/Codegen/Thy/Further.thy
--- 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.
 *}
 
 
diff -r 090dac52cfd7 -r 8fd36f8a5cb7 doc-src/Codegen/Thy/Refinement.thy
--- 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:
 *}
 
diff -r 090dac52cfd7 -r 8fd36f8a5cb7 doc-src/Codegen/Thy/document/Further.tex
--- 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%
 %
diff -r 090dac52cfd7 -r 8fd36f8a5cb7 doc-src/Codegen/Thy/document/Refinement.tex
--- 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%