src/Pure/General/print_mode.ML
changeset 65077 2d6e716c9d6e
parent 62889 99c7f31615c2
equal deleted inserted replaced
65076:8a96ab58f016 65077:2d6e716c9d6e