src/HOL/ex/svc_funcs.ML
changeset 50610 d9c4fbbb0c11
parent 44064 5bce8ff0d9ae
child 51940 958d439b3013