src/HOL/ex/svc_funcs.ML
changeset 35550 e2bc7f8d8d51
parent 35267 8dfd816713c6
child 38549 d0385f2764d8