src/Pure/morphism.ML
changeset 67263 449a989f42cd
parent 62819 d3ff367a16a0
child 67650 5e4f9a0ffea5
equal deleted inserted replaced
67262:46540a2ead4b 67263:449a989f42cd