src/Pure/Syntax/syn_ext.ML
changeset 558 c4092ae47210
parent 555 a7f397a14b16
child 624 33b9b5da3e6f