equal
deleted
inserted
replaced
234 val string_of_time = ATP_Util.string_of_time |
234 val string_of_time = ATP_Util.string_of_time |
235 |
235 |
236 val subscript = implode o map (prefix "\<^sub>") o Symbol.explode |
236 val subscript = implode o map (prefix "\<^sub>") o Symbol.explode |
237 |
237 |
238 fun nat_subscript n = |
238 fun nat_subscript n = |
239 n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript |
239 n |> signed_string_of_int |> not (print_mode_active Print_Mode.ASCII) ? subscript |
240 |
240 |
241 fun flip_polarity Pos = Neg |
241 fun flip_polarity Pos = Neg |
242 | flip_polarity Neg = Pos |
242 | flip_polarity Neg = Pos |
243 | flip_polarity Neut = Neut |
243 | flip_polarity Neut = Neut |
244 |
244 |