src/HOL/Tools/res_lib.ML
changeset 16123 1381e90c2694
parent 15774 9df37a0e935d
child 16515 7896ea4f3a87