src/Pure/Syntax/syn_ext.ML
changeset 37175 be764a7adb10
parent 35429 afa8cf9e63d8
child 37216 3165bc303f66