src/HOL/ex/svc_funcs.ML
changeset 33175 2083bde13ce1
parent 32740 9dd0a2f83429
child 34974 18b41bba42b5