src/Pure/morphism.ML
changeset 29283 f4743512b12d
parent 28965 1de908189869
child 29581 b3b33e0298eb
equal deleted inserted replaced
29282:40a1014cefaa 29283:f4743512b12d