src/Pure/morphism.ML
changeset 35045 a77d200e6503
parent 29605 f2924219125e
child 37216 3165bc303f66
equal deleted inserted replaced
35044:7c761a4bd91f 35045:a77d200e6503