src/HOL/ex/svc_funcs.ML
changeset 57874 9c361f94b323
parent 56256 1e01c159e7d9