src/Pure/type.ML
changeset 80395 46135b44b1a3
parent 79470 9fcf73580c62
equal deleted inserted replaced
80394:348e10664e0f 80395:46135b44b1a3