equal
deleted
inserted
replaced
109 * Metis prover is now an order of magnitude faster, and also works |
109 * Metis prover is now an order of magnitude faster, and also works |
110 with multithreading. |
110 with multithreading. |
111 |
111 |
112 |
112 |
113 *** ML *** |
113 *** ML *** |
|
114 |
|
115 * ML within Isar: antiquotation @{const name} or @{const |
|
116 name(typargs)} produces statically-checked Const term. |
114 |
117 |
115 * The ``print mode'' is now a thread-local value derived from a global |
118 * The ``print mode'' is now a thread-local value derived from a global |
116 template (the former print_mode reference), thus access becomes |
119 template (the former print_mode reference), thus access becomes |
117 non-critical. The global print_mode reference is for session |
120 non-critical. The global print_mode reference is for session |
118 management only; user-code should use print_mode_value, |
121 management only; user-code should use print_mode_value, |