--- a/src/Doc/Codegen/Adaptation.thy Sun Feb 17 19:39:00 2013 +0100
+++ b/src/Doc/Codegen/Adaptation.thy Sun Feb 17 20:45:49 2013 +0100
@@ -119,7 +119,7 @@
The @{theory HOL} @{theory Main} theory already provides a code
generator setup which should be suitable for most applications.
Common extensions and modifications are available by certain
- theories of the @{text HOL} library; beside being useful in
+ theories in @{text "HOL/Library"}; beside being useful in
applications, they may serve as a tutorial for customising the code
generator setup (see below \secref{sec:adaptation_mechanisms}).
--- a/src/Doc/Codegen/Further.thy Sun Feb 17 19:39:00 2013 +0100
+++ b/src/Doc/Codegen/Further.thy Sun Feb 17 20:45:49 2013 +0100
@@ -219,6 +219,14 @@
*}
+subsection {* Parallel computation *}
+
+text {*
+ Theory @{text Parallel} in @{text "HOL/Library"} contains
+ operations to exploit parallelism inside the Isabelle/ML
+ runtime engine.
+*}
+
subsection {* Imperative data structures *}
text {*