src/HOL/ex/svc_funcs.ML
changeset 35144 8b8302da3a55
parent 35092 cfe605c54e50
child 35267 8dfd816713c6