src/Pure/type.ML
changeset 79868 ede8b298cfe8
parent 79470 9fcf73580c62
child 81515 44c0028486db
equal deleted inserted replaced
79867:741b52cb497c 79868:ede8b298cfe8