src/Pure/morphism.ML
changeset 78659 b5f3d1051b13
parent 78112 10487f6571bc
child 78759 461e924cc825