src/Pure/morphism.ML
changeset 72470 e2e9ef9aa2df
parent 70310 c82f59c47aaf
child 74220 c49134ee16c1
equal deleted inserted replaced
72459:15fc6320da68 72470:e2e9ef9aa2df