src/Pure/General/markup.ML
changeset 42669 04dfffda5671
parent 42492 83c57d850049
child 43432 224006e5ac46
equal deleted inserted replaced
42668:b98f22593f97 42669:04dfffda5671