equal
deleted
inserted
replaced
541 the proof context discipline. |
541 the proof context discipline. |
542 |
542 |
543 |
543 |
544 *** System *** |
544 *** System *** |
545 |
545 |
|
546 * Global session timeout is multiplied by timeout_scale factor. This |
|
547 allows to adjust large-scale tests (e.g. AFP) to overall hardware |
|
548 performance. |
|
549 |
546 * Property values in etc/symbols may contain spaces, if written with the |
550 * Property values in etc/symbols may contain spaces, if written with the |
547 replacement character "␣" (Unicode point 0x2324). For example: |
551 replacement character "␣" (Unicode point 0x2324). For example: |
548 |
552 |
549 \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono |
553 \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono |
550 |
554 |
551 * Command-line tool "isabelle update_then" expands old Isar command |
555 * Command-line tool "isabelle update_then" expands old Isar command |
552 conflations: |
556 conflations: |
553 |
557 |
554 hence ~> then have |
558 hence ~> then have |