src/Pure/Syntax/syn_ext.ML
changeset 12804 163a85ba885b
parent 12785 27debaf2112d
child 12865 6b3484b8d572
equal deleted inserted replaced
12803:37131c76dff6 12804:163a85ba885b