src/HOL/ex/svc_funcs.ML
changeset 56544 b60d5d119489
parent 56256 1e01c159e7d9