src/HOL/ex/svc_funcs.ML
changeset 42224 578a51fae383
parent 38864 4abe644fcea5
child 42364 8c674b3b8e44