src/Pure/type.ML
changeset 15975 cc4821a9f1b1
parent 15797 a63605582573
child 16289 958207815931