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