src/HOL/ex/svc_funcs.ML
changeset 42380 9371ea9f91fb
parent 42364 8c674b3b8e44
child 43850 7f2cbc713344