src/Pure/pure_syn.ML
changeset 52131 366fa32ee2a3
parent 48905 04576657cf94
child 52455 9a8f4fdac3cf