src/Pure/General/markup.ML
changeset 26931 aa226d8405a8
parent 26702 a079f8f0080b
child 26977 e736139b553d
equal deleted inserted replaced
26930:64e50d783276 26931:aa226d8405a8