src/HOL/Tools/choice_specification.ML
changeset 79531 22a137a6de44
parent 79412 1c758cd8d5b2
child 80636 4041e7c8059d