src/Pure/type.ML
changeset 79980 ee04ce2ac13f
parent 79470 9fcf73580c62
child 81515 44c0028486db
equal deleted inserted replaced
79979:a4100b7ab951 79980:ee04ce2ac13f