src/HOL/ex/svc_funcs.ML
changeset 56330 5c4d3be7a6b0
parent 56256 1e01c159e7d9