src/HOL/ex/svc_funcs.ML
changeset 21213 c81f016883df
parent 21078 101aefd61aac
child 21395 f34ac19659ae