src/Pure/Syntax/sextension.ML
changeset 10120 0f315aeee16e
parent 473 fdacecc688a1