src/Pure/morphism.ML
changeset 66475 d8e0fd64216f
parent 62819 d3ff367a16a0
child 67650 5e4f9a0ffea5