src/HOL/Tools/res_lib.ML
changeset 15872 8336ff711d80
parent 15774 9df37a0e935d
child 16515 7896ea4f3a87