equal
deleted
inserted
replaced
54 %x. c. The simplifier setup is now more robust against eta expansion. |
54 %x. c. The simplifier setup is now more robust against eta expansion. |
55 INCOMPATIBILITY: in cases explicitly referring to K_record. |
55 INCOMPATIBILITY: in cases explicitly referring to K_record. |
56 |
56 |
57 * Metis prover is now an order of magnitude faster, and also works |
57 * Metis prover is now an order of magnitude faster, and also works |
58 with multithreading. |
58 with multithreading. |
|
59 |
|
60 |
|
61 *** ML *** |
|
62 |
|
63 * The ``print mode'' is now a thread-local value derived from a global |
|
64 template (the former print_mode reference), thus access becomes |
|
65 non-critical. The global print_mode reference is for session |
|
66 management only; user-code should use print_mode_value, |
|
67 print_mode_active, PrintMode.setmp etc. INCOMPATIBILITY. |
59 |
68 |
60 |
69 |
61 *** System *** |
70 *** System *** |
62 |
71 |
63 * isatool tty runs Isabelle process with plain tty interaction; |
72 * isatool tty runs Isabelle process with plain tty interaction; |