src/HOL/ex/svc_funcs.ML
changeset 19597 8ced57ffc090
parent 19336 fb5e19d26d5e
child 20853 3ff5a2e05810
equal deleted inserted replaced
19596:7b07dac44e09 19597:8ced57ffc090