src/Pure/morphism.ML
changeset 62047 1ae53588dcbb
parent 61064 01b23bfb4947
child 62505 9e2a65912111