src/Pure/pure_syn.ML
changeset 55736 f1ed1e9cd080
parent 54450 7815563f50dc
child 55788 67699e08e969