src/HOL/Tools/choice_specification.ML
changeset 79531 22a137a6de44
parent 79412 1c758cd8d5b2
child 80636 4041e7c8059d
equal deleted inserted replaced
79530:1b0fc6ceb750 79531:22a137a6de44