src/Pure/morphism.ML
changeset 53853 e8430d668f44
parent 53087 5a1dcda7967c
child 54740 91f54d386680
equal deleted inserted replaced
53852:c7707223d782 53853:e8430d668f44