# HG changeset patch
# User haftmann
# Date 1361130349 -3600
# Node ID 16eb76ca1e4afdd8e53af61bfd2466c3d92fcdc1
# Parent  e8b2d90da4998129c4891506d8d63e979a722174
note on parallel computation

diff -r e8b2d90da499 -r 16eb76ca1e4a src/Doc/Codegen/Adaptation.thy
--- 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}).
 
diff -r e8b2d90da499 -r 16eb76ca1e4a src/Doc/Codegen/Further.thy
--- 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 {*