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 Spec_Check
imports Main
begin
ML_file "random.ML"
ML_file "property.ML"
ML_file "base_generator.ML"
ML_file "generator.ML"
ML_file "gen_construction.ML"
ML_file "spec_check.ML"
ML_file "output_style.ML"
setup Output_Style.setup
end