src/Pure/morphism.ML
changeset 26457 9385d441cec6
parent 24031 e94e541346d7
child 28074 90adbbf03187
equal deleted inserted replaced
26456:a63501938ce1 26457:9385d441cec6