src/Pure/morphism.ML
changeset 65276 fa1a5efee2ec
parent 62819 d3ff367a16a0
child 67650 5e4f9a0ffea5