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