equal
deleted
inserted
replaced
3 |
3 |
4 New in this Isabelle version |
4 New in this Isabelle version |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
|
8 |
|
9 * Theorem status about oracles and unfinished/failed future proofs is |
|
10 no longer printed by default, since it is incompatible with |
|
11 incremental / parallel checking of the persistent document model. ML |
|
12 function Thm.peek_status may be used to inspect a snapshot of the |
|
13 ongoing evaluation process. Note that in batch mode --- notably |
|
14 isabelle build --- the system ensures that future proofs of all |
|
15 accessible theorems in the theory context are finished (as before). |
8 |
16 |
9 * Configuration option show_markup controls direct inlining of markup |
17 * Configuration option show_markup controls direct inlining of markup |
10 into the printed representation of formal entities --- notably type |
18 into the printed representation of formal entities --- notably type |
11 and sort constraints. This enables Prover IDE users to retrieve that |
19 and sort constraints. This enables Prover IDE users to retrieve that |
12 information via tooltips in the output window, for example. |
20 information via tooltips in the output window, for example. |