src/HOL/ex/svc_funcs.ML
changeset 59362 41f1645a4f63
parent 56256 1e01c159e7d9