src/HOL/ex/svc_funcs.ML
changeset 40870 94427db32392
parent 38864 4abe644fcea5
child 42364 8c674b3b8e44