src/Pure/pure_syn.ML
changeset 55215 b6c926e67350
parent 54450 7815563f50dc
child 55788 67699e08e969