src/HOL/Tools/split_rule.ML
changeset 76404 4de3d831ff4d
parent 74282 c2ee8d993d6a
child 77879 dd222e2af01a
equal deleted inserted replaced
76403:fb9c567a67cd 76404:4de3d831ff4d