src/Pure/ROOT.ML
changeset 13224 6f0928a942d1
parent 12778 3120e338ffae
child 13271 d0859ff6cd65
equal deleted inserted replaced
13223:45be08fbdcff 13224:6f0928a942d1