src/Pure/type.ML
changeset 20854 f9cf9e62d11c
parent 20674 93baed0f741c
child 20951 868120282837