src/HOL/ex/svc_funcs.ML
changeset 17184 3d80209e9a53
parent 16836 45a3dc4688bc
child 17465 93fc1211603f