src/Pure/morphism.ML
changeset 62296 b04a5ddd6121
parent 61064 01b23bfb4947
child 62505 9e2a65912111