src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 62337 d3996d5873dd
parent 61760 1647bb489522
child 62320 dc8374620332