src/Pure/Syntax/syn_trans.ML
changeset 33819 cad5c38373d8
parent 32786 f1ac4b515af9
child 35145 f132a4fd8679
equal deleted inserted replaced
33818:aa00c583f594 33819:cad5c38373d8