src/Pure/General/yxml.ML
changeset 43782 834de29572d5
parent 43777 22c87ff1b8a9
equal deleted inserted replaced
43781:d43e5f79bdc2 43782:834de29572d5
    50 val X = chr 5;
    50 val X = chr 5;
    51 val Y = chr 6;
    51 val Y = chr 6;
    52 val XY = X ^ Y;
    52 val XY = X ^ Y;
    53 val XYX = XY ^ X;
    53 val XYX = XY ^ X;
    54 
    54 
    55 val detect = exists_string (fn s => s = X);
    55 val detect = exists_string (fn s => s = X orelse s = Y);
    56 
    56 
    57 
    57 
    58 (* output *)
    58 (* output *)
    59 
    59 
    60 fun output_markup (markup as (name, atts)) =
    60 fun output_markup (markup as (name, atts)) =