# 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 {*