src/HOL/ex/svc_funcs.ML
changeset 40046 ba2e41c8b725
parent 38864 4abe644fcea5
child 42364 8c674b3b8e44