section ‹Default instances› theory Eval_Instances imports Embed begin ML_file "eval_instances.ML" setup ‹Eval_Instances.setup› derive evaluate nat bool list unit prod sum option char num name "term" end