src/HOL/Tools/res_lib.ML
changeset 16240 95cc0e8f8a17
parent 15774 9df37a0e935d
child 16515 7896ea4f3a87