src/HOL/Tools/split_rule.ML
changeset 24027 a1afcff544a6
parent 22278 70a7cd02fec1
child 24584 01e83ffa6c54
equal deleted inserted replaced
24026:8a4d5312d378 24027:a1afcff544a6