src/Pure/Syntax/syn_ext.ML
changeset 33205 20587741a8d9
parent 33042 ddf1f03a9ad9
child 33317 b4534348b8fd