src/HOL/ex/svc_funcs.ML
changeset 21635 32f3e1127de2
parent 21395 f34ac19659ae
child 21820 2f2b6a965ccc