src/Pure/morphism.ML
changeset 82702 32dd31062eaa
parent 80809 4a64fc4d1cde