equal
deleted
inserted
replaced
1 section \<open>A simple example demonstrating parallelism for code generated towards Isabelle/ML\<close> |
1 section \<open>A simple example demonstrating parallelism for code generated towards Isabelle/ML\<close> |
2 |
2 |
3 theory Parallel_Example |
3 theory Parallel_Example |
4 imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug" |
4 imports Complex_Main "HOL-Library.Parallel" "HOL-Library.Debug" |
5 begin |
5 begin |
6 |
6 |
7 subsection \<open>Compute-intensive examples.\<close> |
7 subsection \<open>Compute-intensive examples.\<close> |
8 |
8 |
9 subsubsection \<open>Fragments of the harmonic series\<close> |
9 subsubsection \<open>Fragments of the harmonic series\<close> |