src/HOL/ex/svc_funcs.ML
changeset 15384 b13eb8a8897d
parent 14982 ff1c919f4982
child 15531 08c8dad8e399
equal deleted inserted replaced
15383:c49e4225ef4f 15384:b13eb8a8897d