src/HOL/ex/svc_funcs.ML
changeset 24461 bbff04c027ec
parent 23881 851c74f1bb69
child 24584 01e83ffa6c54