src/Pure/pure_syn.ML
changeset 66820 fc516da7ee4f
parent 64556 851ae0e7b09c
child 67381 146757999c8d
equal deleted inserted replaced
66819:064c80e9d1cf 66820:fc516da7ee4f