src/HOL/Tools/choice_specification.ML
changeset 69272 15e9ed5b28fb
parent 67149 e61557884799
child 74233 9eff7c673b42