src/HOL/Tools/split_rule.ML
changeset 24930 cc2e0e8c81af
parent 24584 01e83ffa6c54
child 25979 3297781f8141