src/Pure/morphism.ML
changeset 78086 5edd5b12017d
parent 78085 dd7bb7f99ad5
child 78089 52d071212a7a