src/Pure/Syntax/syn_ext.ML
changeset 36944 dbf831a50e4a
parent 35429 afa8cf9e63d8
child 37216 3165bc303f66
equal deleted inserted replaced
36943:ae740b96b914 36944:dbf831a50e4a