src/HOL/Tools/split_rule.ML
changeset 55684 ee49b4f7edc8
parent 51717 9e7d1c139569
child 58468 d1f6a38f9415
equal deleted inserted replaced
55683:5732a55b9232 55684:ee49b4f7edc8