src/HOL/ex/svc_funcs.ML
changeset 43223 c9e87dc92d9e
parent 42364 8c674b3b8e44
child 43850 7f2cbc713344