src/Pure/morphism.ML
changeset 58874 7172c7ffb047
parent 54740 91f54d386680
child 61064 01b23bfb4947
equal deleted inserted replaced
58873:db866dc081f8 58874:7172c7ffb047