src/Pure/morphism.ML
changeset 22264 6a65e9b2ae05
parent 22235 6eac7f7c3294
child 22571 3f00e937d1c9