[isabelle-dev] NEWS

* ML: ``print mode'' is now a thread-local value derived from a global template (the former print_mode reference), thus access becomes non-critical. The global print_mode reference is for session management only; user-code should use print_mode_value, print_mode_active, PrintMode.setmp etc. INCOM

[isabelle-dev] NEWS

* Metis prover is now an order of magnitude faster, and also works with multithreading.