src/HOL/ex/svc_funcs.ML
changeset 38630 2479d541bc61
parent 38558 32ad17fe2b9c
child 38786 e46e7a9cb622