src/HOL/ex/svc_funcs.ML
changeset 26964 df1f238a05f7
parent 26939 1035c89b4c02
child 28290 4cc2b6046258