src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 66020 a31760eee09d
parent 62752 d09d71223e7a
child 69593 3dda49e08b9d
equal deleted inserted replaced
66019:69b5ef78fb07 66020:a31760eee09d
    67   val empty = []
    67   val empty = []
    68   val extend = I
    68   val extend = I
    69   fun merge data = AList.merge (op =) (K true) data
    69   fun merge data = AList.merge (op =) (K true) data
    70 )
    70 )
    71 
    71 
    72 fun xsym s s' () = if print_mode_active Symbol.xsymbolsN then s else s'
    72 fun xsym s s' () = if not (print_mode_active Print_Mode.ASCII) then s else s'
    73 
    73 
    74 val irrelevant = "_"
    74 val irrelevant = "_"
    75 val unknown = "?"
    75 val unknown = "?"
    76 val unrep_mixfix = xsym "\<dots>" "..."
    76 val unrep_mixfix = xsym "\<dots>" "..."
    77 val maybe_mixfix = xsym "_\<^sup>?" "_?"
    77 val maybe_mixfix = xsym "_\<^sup>?" "_?"