src/Pure/Syntax/syn_ext.ML
changeset 670 ff4c6691de9d
parent 624 33b9b5da3e6f
child 764 b60e77395d1a