src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 72922 d78bd4432f05
parent 72450 24bd1316eaae
child 73761 ef1a18e20ace