src/Pure/Tools/am_util.ML
changeset 22722 704de05715b4
parent 17799 1cc6e60bd5ff
equal deleted inserted replaced
22721:d9be18bd7a28 22722:704de05715b4