src/Pure/Syntax/syn_ext.ML
changeset 36592 eacded3b05f7
parent 35429 afa8cf9e63d8
child 37216 3165bc303f66
equal deleted inserted replaced
36591:df38e0c5c123 36592:eacded3b05f7