src/HOL/Tools/split_rule.ML
changeset 24432 d555d941f983
parent 22278 70a7cd02fec1
child 24584 01e83ffa6c54
equal deleted inserted replaced
24431:02d29baa42ff 24432:d555d941f983