src/Pure/morphism.ML
changeset 62890 728aa05e9433
parent 62819 d3ff367a16a0
child 67650 5e4f9a0ffea5
equal deleted inserted replaced
62889:99c7f31615c2 62890:728aa05e9433