note on parallel computation
authorhaftmann
Sun Feb 17 20:45:49 2013 +0100 (2013-02-17)
changeset 5117216eb76ca1e4a
parent 51171 e8b2d90da499
child 51173 3cbb4e95a565
note on parallel computation
src/Doc/Codegen/Adaptation.thy
src/Doc/Codegen/Further.thy
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Sun Feb 17 19:39:00 2013 +0100
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Sun Feb 17 20:45:49 2013 +0100
     1.3 @@ -119,7 +119,7 @@
     1.4    The @{theory HOL} @{theory Main} theory already provides a code
     1.5    generator setup which should be suitable for most applications.
     1.6    Common extensions and modifications are available by certain
     1.7 -  theories of the @{text HOL} library; beside being useful in
     1.8 +  theories in @{text "HOL/Library"}; beside being useful in
     1.9    applications, they may serve as a tutorial for customising the code
    1.10    generator setup (see below \secref{sec:adaptation_mechanisms}).
    1.11  
     2.1 --- a/src/Doc/Codegen/Further.thy	Sun Feb 17 19:39:00 2013 +0100
     2.2 +++ b/src/Doc/Codegen/Further.thy	Sun Feb 17 20:45:49 2013 +0100
     2.3 @@ -219,6 +219,14 @@
     2.4  *}
     2.5  
     2.6  
     2.7 +subsection {* Parallel computation *}
     2.8 +
     2.9 +text {*
    2.10 +  Theory @{text Parallel} in @{text "HOL/Library"} contains
    2.11 +  operations to exploit parallelism inside the Isabelle/ML
    2.12 +  runtime engine.
    2.13 +*}
    2.14 +
    2.15  subsection {* Imperative data structures *}
    2.16  
    2.17  text {*