src/Pure/Syntax/sextension.ML
changeset 189 831a9a7ab9f3
parent 165 793be9f1e88e
child 238 6af40e3a2bcb