✐‹creator "Kevin Kappelmann"› section ‹Costs and Priorities› theory ML_Costs_Priorities imports ML_Parsing_Utils begin paragraph ‹Summary› text ‹Costs and priorities for ML tactics.› ML_file‹cost_priority.ML› end