src/HOL/ex/svc_funcs.ML
changeset 59973 a51af4f12d47
parent 56256 1e01c159e7d9