src/HOL/ex/svc_funcs.ML
changeset 27824 97d2a3797ce0
parent 26939 1035c89b4c02
child 28290 4cc2b6046258