src/HOL/Tools/choice_specification.ML
changeset 43615 8e0f6cfa8eb2
parent 42361 23f352990944
child 44121 44adaa6db327
equal deleted inserted replaced
43614:2c741b50d4b7 43615:8e0f6cfa8eb2