src/HOL/Tools/choice_specification.ML
changeset 33037 b22e44496dc2
parent 32957 675c0c7e6a37
child 33245 65232054ffd0
equal deleted inserted replaced
33015:575bd6548df9 33037:b22e44496dc2