src/HOL/ex/svc_funcs.ML
changeset 17459 9a3925c07392
parent 16836 45a3dc4688bc
child 17465 93fc1211603f