src/HOL/ex/svc_funcs.ML
changeset 43152 6c4e021dec06
parent 42364 8c674b3b8e44
child 43850 7f2cbc713344