disallow concurrent execution attempt explicitly -- it should never happen due to management of singleton execution;
tuned error messages: prefer plain "error" as in document.ML;
theory Hoare_Parallel
imports OG_Examples Gar_Coll Mul_Gar_Coll RG_Examples
begin
end