src/HOL/Tools/res_lib.ML
changeset 17740 fc385ce6187d
parent 17525 ae5bb6001afb
child 17764 fde495b9e24b