src/Pure/Syntax/ROOT.ML
changeset 194 06e31ac55dd1
parent 163 ad90d96c2ec3
child 239 08b6e842ec16
equal deleted inserted replaced
193:b2be328e00c3 194:06e31ac55dd1