src/HOL/ex/svc_funcs.ML
changeset 28437 0790f66a931a
parent 28290 4cc2b6046258
child 29276 94b1ffec9201