src/HOL/Tools/split_rule.ML
changeset 53470 fe80dd7cd543
parent 51717 9e7d1c139569
child 58468 d1f6a38f9415
equal deleted inserted replaced
53469:3356a148b783 53470:fe80dd7cd543