src/HOL/Tools/split_rule.ML
changeset 33118 973d18ad2a73
parent 32342 3fabf5b5fc83
child 33368 b1cf34f1855c