src/HOL/Tools/split_rule.ML
changeset 16071 e0136cdef722
parent 15661 9ef583b08647
child 18050 652c95961a8b
equal deleted inserted replaced
16070:4a83dd540b88 16071:e0136cdef722