src/HOL/Tools/split_rule.ML
changeset 56812 baef1c110f12
parent 51717 9e7d1c139569
child 58468 d1f6a38f9415
equal deleted inserted replaced
56811:b66639331db5 56812:baef1c110f12