src/HOL/Tools/split_rule.ML
changeset 81945 23957ebffaf7
parent 77879 dd222e2af01a
equal deleted inserted replaced
81944:234912588ffe 81945:23957ebffaf7