src/HOL/ex/svc_funcs.ML
changeset 29183 f1648e009dc1
parent 28290 4cc2b6046258
child 29276 94b1ffec9201