src/Pure/General/markup.ML
changeset 27903 af1b39debf30
parent 27894 a06f78f917e0
child 27969 46d7057b8614
equal deleted inserted replaced
27902:4a419fd52f44 27903:af1b39debf30