src/HOL/Tools/split_rule.ML
changeset 60620 41e180848d02
parent 60363 5568b16aa477
child 60642 48dd1cefb4ae
equal deleted inserted replaced
60616:5a65c496d96f 60620:41e180848d02