src/Pure/type.ML
changeset 59804 db0b87085c16
parent 59058 a78612c67ec0
child 59841 2551ac44150e