src/HOL/ex/svc_funcs.ML
changeset 42078 d5bf0ce40bd7
parent 38864 4abe644fcea5
child 42364 8c674b3b8e44