src/HOL/Tools/split_rule.ML
changeset 74766 71a447e4073b
parent 74282 c2ee8d993d6a
child 77879 dd222e2af01a