src/Pure/morphism.ML
changeset 28337 93964076e7b8
parent 28074 90adbbf03187
child 28965 1de908189869