src/HOL/Tools/split_rule.ML
changeset 18052 004515accc10
parent 18050 652c95961a8b
child 18629 bdf01da93ed4
equal deleted inserted replaced
18051:dba086ed50cb 18052:004515accc10