src/Pure/General/print_mode.ML
changeset 79899 c73a36081b1c
parent 62889 99c7f31615c2
child 80861 9de19e3a7231
equal deleted inserted replaced
79898:db9a45e05b5b 79899:c73a36081b1c