equal
deleted
inserted
replaced
405 time. For the default print mode, both Output.output and Output.raw |
405 time. For the default print mode, both Output.output and Output.raw |
406 have no effect. |
406 have no effect. |
407 |
407 |
408 * Pure: print_tac now outputs the goal through the trace channel. |
408 * Pure: print_tac now outputs the goal through the trace channel. |
409 |
409 |
410 * Isar debugging: new reference Toplevel.debug; default false. Set to |
410 * Isar debugging: new reference Toplevel.debug (default false). Set |
411 make printing of exceptions THM, TERM, TYPE and THEORY more verbose. |
411 to make printing of exceptions THM, TERM, TYPE and THEORY more |
|
412 verbose. |
|
413 |
|
414 * Isar profiling: new reference Toplevel.profiling (default 0). For |
|
415 Poly/ML, set to 1 to profile time, 2 to profile space (which increases |
|
416 the runtime). |
412 |
417 |
413 * Pure: name spaces have been refined, with significant changes of the |
418 * Pure: name spaces have been refined, with significant changes of the |
414 internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table) |
419 internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table) |
415 to extern(_table). The plain name entry path is superceded by a |
420 to extern(_table). The plain name entry path is superceded by a |
416 general 'naming' context, which also includes the 'policy' to produce |
421 general 'naming' context, which also includes the 'policy' to produce |