src/HOL/ex/svc_funcs.ML
changeset 22473 753123c89d72
parent 21962 279b129498b6
child 22997 d4f3b015b50b