src/Pure/morphism.ML
changeset 24978 159b0f4dd1e9
parent 24031 e94e541346d7
child 28074 90adbbf03187
equal deleted inserted replaced
24977:9f98751c9628 24978:159b0f4dd1e9