src/HOL/ex/svc_funcs.ML
changeset 23277 aa158e145ea3
parent 22997 d4f3b015b50b
child 23881 851c74f1bb69