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