src/Pure/General/markup.ML
changeset 38796 c421cfe2eada
parent 38721 ca8b14fa0d0d
child 38871 28496da3bec2
equal deleted inserted replaced
38793:eba0175d4cd1 38796:c421cfe2eada