src/HOL/Tools/choice_specification.ML
changeset 80026 a03a7d4b82f8
parent 79412 1c758cd8d5b2
child 80636 4041e7c8059d