src/Pure/type.ML
changeset 82458 c7bd567723b1
parent 81991 c61434d8558e
equal deleted inserted replaced
82457:5a0d1075911c 82458:c7bd567723b1