HOL-ex.Parallel_Example