src/HOL/ex/svc_funcs.ML
changeset 20864 bb75b876b260
parent 20853 3ff5a2e05810
child 21078 101aefd61aac