equal
deleted
inserted
replaced
20 |
20 |
21 * Fact collection sign_simps contains only simplification rules |
21 * Fact collection sign_simps contains only simplification rules |
22 for products being less / greater / equal to zero; combine with |
22 for products being less / greater / equal to zero; combine with |
23 existing collections algebra_simps or field_simps to obtain |
23 existing collections algebra_simps or field_simps to obtain |
24 reasonable simplification. INCOMPATIBILITY. |
24 reasonable simplification. INCOMPATIBILITY. |
|
25 |
|
26 * Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) associates |
|
27 to the left now as is customary. |
25 |
28 |
26 |
29 |
27 New in Isabelle2019 (June 2019) |
30 New in Isabelle2019 (June 2019) |
28 ------------------------------- |
31 ------------------------------- |
29 |
32 |
3185 * Global session timeout is multiplied by timeout_scale factor. This |
3188 * Global session timeout is multiplied by timeout_scale factor. This |
3186 allows to adjust large-scale tests (e.g. AFP) to overall hardware |
3189 allows to adjust large-scale tests (e.g. AFP) to overall hardware |
3187 performance. |
3190 performance. |
3188 |
3191 |
3189 * Property values in etc/symbols may contain spaces, if written with the |
3192 * Property values in etc/symbols may contain spaces, if written with the |
3190 replacement character "␣" (Unicode point 0x2324). For example: |
3193 replacement character "?" (Unicode point 0x2324). For example: |
3191 |
3194 |
3192 \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono |
3195 \<star> code: 0x0022c6 group: operator font: Deja?Vu?Sans?Mono |
3193 |
3196 |
3194 * Java runtime environment for x86_64-windows allows to use larger heap |
3197 * Java runtime environment for x86_64-windows allows to use larger heap |
3195 space. |
3198 space. |
3196 |
3199 |
3197 * Java runtime options are determined separately for 32bit vs. 64bit |
3200 * Java runtime options are determined separately for 32bit vs. 64bit |