src/Pure/General/markup.ML
changeset 29606 fedb8be05f24
parent 29522 793766d4c1b5
child 30221 14145e81a2fe
equal deleted inserted replaced
29605:f2924219125e 29606:fedb8be05f24