src/HOL/Tools/split_rule.ML
changeset 23277 aa158e145ea3
parent 22278 70a7cd02fec1
child 24584 01e83ffa6c54