src/Pure/morphism.ML
changeset 65371 ce09e947c1d5
parent 62819 d3ff367a16a0
child 67650 5e4f9a0ffea5