src/HOL/ex/svc_funcs.ML
changeset 15916 1314ef1e49dd
parent 15574 b1d1b5bfc464
child 15965 f422f8283491