src/HOL/Tools/res_lib.ML
changeset 16407 e3c3405613c5
parent 15774 9df37a0e935d
child 16515 7896ea4f3a87
equal deleted inserted replaced
16406:4f393b8f84b7 16407:e3c3405613c5