src/HOL/Tools/split_rule.ML
changeset 16407 e3c3405613c5
parent 15661 9ef583b08647
child 18050 652c95961a8b