src/HOL/Tools/svc_funcs.ML
changeset 7742 01386eb4eab0
parent 7545 1578f1fd62cf
child 10892 405b077433a3
equal deleted inserted replaced
7741:874abb8aa65b 7742:01386eb4eab0