src/HOL/ex/svc_funcs.ML
changeset 59614 452458cf8506
parent 56256 1e01c159e7d9